reconsider F = Fin X as Subset-Family of X by FINSUB_1:13;
reconsider XX = {X} as Subset-Family of X by ZFMISC_1:68;
set IT = CofinTop X;
reconsider XX = XX as Subset-Family of X ;
reconsider F = F as Subset-Family of X ;
A1: the carrier of (CofinTop X) = X by Def6;
A2: COMPLEMENT the topology of (CofinTop X) = {X} \/ (Fin X) by Def6;
A3: the topology of (CofinTop X) = COMPLEMENT (COMPLEMENT the topology of (CofinTop X))
.= (COMPLEMENT XX) \/ (COMPLEMENT F) by A1, A2, SETFAM_1:39
.= {{}} \/ (COMPLEMENT F) by SETFAM_1:40 ;
{}. X in F ;
then (({} X) `) ` in F ;
then [#] X in COMPLEMENT F by SETFAM_1:def 7;
hence the carrier of (CofinTop X) in the topology of (CofinTop X) by A1, A3, XBOOLE_0:def 3; :: according to PRE_TOPC:def 1 :: thesis: ( ( for b1 being Element of bool (bool the carrier of (CofinTop X)) holds
( not b1 c= the topology of (CofinTop X) or union b1 in the topology of (CofinTop X) ) ) & ( for b1, b2 being Element of bool the carrier of (CofinTop X) holds
( not b1 in the topology of (CofinTop X) or not b2 in the topology of (CofinTop X) or b1 /\ b2 in the topology of (CofinTop X) ) ) )
A4: {} in {{}} by TARSKI:def 1;
thus for a being Subset-Family of (CofinTop X) st a c= the topology of (CofinTop X) holds
union a in the topology of (CofinTop X) :: thesis: for b1, b2 being Element of bool the carrier of (CofinTop X) holds
( not b1 in the topology of (CofinTop X) or not b2 in the topology of (CofinTop X) or b1 /\ b2 in the topology of (CofinTop X) )
proof
let a be Subset-Family of (CofinTop X); :: thesis: ( a c= the topology of (CofinTop X) implies union a in the topology of (CofinTop X) )
assume A5: a c= the topology of (CofinTop X) ; :: thesis: union a in the topology of (CofinTop X)
set b = a /\ (COMPLEMENT F);
reconsider b = a /\ (COMPLEMENT F) as Subset-Family of X ;
reconsider b = b as Subset-Family of X ;
a /\ {{}} c= {{}} by XBOOLE_1:17;
then ( a /\ {{}} = {{}} or a /\ {{}} = {} ) by ZFMISC_1:33;
then A6: union (a /\ {{}}) = {} by ZFMISC_1:2, ZFMISC_1:25;
A7: union a = union (a /\ the topology of (CofinTop X)) by A5, XBOOLE_1:28
.= union ((a /\ {{}}) \/ (a /\ (COMPLEMENT F))) by A3, XBOOLE_1:23
.= (union (a /\ {{}})) \/ (union (a /\ (COMPLEMENT F))) by ZFMISC_1:78
.= union b by A6 ;
per cases ( b = {} or b <> {} ) ;
end;
end;
let a, b be Subset of (CofinTop X); :: thesis: ( not a in the topology of (CofinTop X) or not b in the topology of (CofinTop X) or a /\ b in the topology of (CofinTop X) )
assume that
A10: a in the topology of (CofinTop X) and
A11: b in the topology of (CofinTop X) ; :: thesis: a /\ b in the topology of (CofinTop X)
reconsider a9 = a, b9 = b as Subset of X by Def6;
per cases ( a = {} or b = {} or ( a <> {} & b <> {} ) ) ;
suppose ( a = {} or b = {} ) ; :: thesis: a /\ b in the topology of (CofinTop X)
hence a /\ b in the topology of (CofinTop X) by A3, A4, XBOOLE_0:def 3; :: thesis: verum
end;
suppose A12: ( a <> {} & b <> {} ) ; :: thesis: a /\ b in the topology of (CofinTop X)
then not b in {{}} by TARSKI:def 1;
then b9 in COMPLEMENT F by A3, A11, XBOOLE_0:def 3;
then A13: b9 ` in Fin X by SETFAM_1:def 7;
not a in {{}} by A12, TARSKI:def 1;
then a9 in COMPLEMENT F by A3, A10, XBOOLE_0:def 3;
then a9 ` in Fin X by SETFAM_1:def 7;
then (a9 `) \/ (b9 `) in Fin X by A13, FINSUB_1:1;
then (a9 /\ b9) ` in Fin X by XBOOLE_1:54;
then a /\ b in COMPLEMENT F by SETFAM_1:def 7;
hence a /\ b in the topology of (CofinTop X) by A3, XBOOLE_0:def 3; :: thesis: verum
end;
end;