proposition: Lemma Exercise6_31_fP x y: inc x F -> inc y F -> (inc y (f x) <-> forall z, infinite_set z -> sub z y -> infinite_set (x \cap z)).
proof: Proof. move => xF yF. move: Exercise6_31_i =>[or sr]. have xsr: inc x (substrate r') by ue. have ysr: inc y (substrate r') by ue. apply: (iff_trans (Exercise1_23e or xsr ysr)). split => hyp. move => z iz szy. move/Zo_P: (yF) => [/Zo_P [/setP_P yA yi] yc]. move: (countable_sub szy yc) => cz. have zF: inc z F. by apply: Zo_i cz; apply:Zo_i iz; apply/setP_P; apply: (sub_trans szy yA). have le1: gle r' y z by apply/Exercise6_31_j. move:(hyp z le1) => [t /Exercise6_31_j [_ tf s1] /Exercise6_31_j [_ _ s2]]. have s3: sub t (x\cap z). move => a ia; apply: setI2_i; [ by apply: s2 | by apply: s1]. exact:(sub_infinite_set s3 (Zo_hi (Zo_S tf))). move => z /Exercise6_31_j [_ zF zy]. move: (hyp _ (Zo_hi (Zo_S zF)) zy) => ii. have siz: sub (x \cap z) z by move => t /setI2_P []. have six: sub (x \cap z) x by move => t /setI2_P []. move/Zo_P: (xF) => [/Zo_P [/setP_P xA _] xc]. have iF: inc (x \cap z) F. apply:Zo_i (countable_sub six xc); apply: Zo_i => //. apply/setP_P; apply: (sub_trans six xA). by exists (x \cap z); apply/Exercise6_31_j. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)