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 () = X by Def6;
A2: COMPLEMENT the topology of () = {X} \/ (Fin X) by Def6;
A3: the topology of () = COMPLEMENT (COMPLEMENT the topology of ())
.= () \/ () by
.= \/ () 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 () in the topology of () by ; :: according to PRE_TOPC:def 1 :: thesis: ( ( for b1 being Element of bool (bool the carrier of ()) holds
( not b1 c= the topology of () or union b1 in the topology of () ) ) & ( for b1, b2 being Element of bool the carrier of () holds
( not b1 in the topology of () or not b2 in the topology of () or b1 /\ b2 in the topology of () ) ) )

A4: {} in by TARSKI:def 1;
thus for a being Subset-Family of () st a c= the topology of () holds
union a in the topology of () :: thesis: for b1, b2 being Element of bool the carrier of () holds
( not b1 in the topology of () or not b2 in the topology of () or b1 /\ b2 in the topology of () )
proof
let a be Subset-Family of (); :: thesis: ( a c= the topology of () implies union a in the topology of () )
assume A5: a c= the topology of () ; :: thesis: union a in the topology of ()
set b = a /\ ();
reconsider b = a /\ () 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 () = {} by ;
A7: union a = union (a /\ the topology of ()) by
.= union (() \/ (a /\ ())) by
.= (union ()) \/ (union (a /\ ())) by ZFMISC_1:78
.= union b by A6 ;
per cases ( b = {} or b <> {} ) ;
end;
end;
let a, b be Subset of (); :: thesis: ( not a in the topology of () or not b in the topology of () or a /\ b in the topology of () )
assume that
A10: a in the topology of () and
A11: b in the topology of () ; :: thesis: a /\ b in the topology of ()
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 ()
hence a /\ b in the topology of () by ; :: thesis: verum
end;
suppose A12: ( a <> {} & b <> {} ) ; :: thesis: a /\ b in the topology of ()
end;
end;