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 b_{1} being Element of bool (bool the carrier of (CofinTop X)) holds

( not b_{1} c= the topology of (CofinTop X) or union b_{1} in the topology of (CofinTop X) ) ) & ( for b_{1}, b_{2} being Element of bool the carrier of (CofinTop X) holds

( not b_{1} in the topology of (CofinTop X) or not b_{2} in the topology of (CofinTop X) or b_{1} /\ b_{2} 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 b_{1}, b_{2} being Element of bool the carrier of (CofinTop X) holds

( not b_{1} in the topology of (CofinTop X) or not b_{2} in the topology of (CofinTop X) or b_{1} /\ b_{2} 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;

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 b

( not b

( not b

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 b

( not b

proof

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) )
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 ;

end;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;

suppose
b = {}
; :: thesis: union a in the topology of (CofinTop X)

hence
union a in the topology of (CofinTop X)
by A3, A4, A7, XBOOLE_0:def 3, ZFMISC_1:2; :: thesis: verum

end;suppose A8:
b <> {}
; :: thesis: union a in the topology of (CofinTop X)

b c= COMPLEMENT F
by XBOOLE_1:17;

then A9: COMPLEMENT b c= Fin X by SETFAM_1:37;

meet (COMPLEMENT b) = ([#] X) \ (union b) by A8, SETFAM_1:33

.= (union b) ` ;

then (union b) ` in Fin X by A9, Th2;

then union b in COMPLEMENT F by SETFAM_1:def 7;

hence union a in the topology of (CofinTop X) by A3, A7, XBOOLE_0:def 3; :: thesis: verum

end;then A9: COMPLEMENT b c= Fin X by SETFAM_1:37;

meet (COMPLEMENT b) = ([#] X) \ (union b) by A8, SETFAM_1:33

.= (union b) ` ;

then (union b) ` in Fin X by A9, Th2;

then union b in COMPLEMENT F by SETFAM_1:def 7;

hence union a in the topology of (CofinTop X) by A3, A7, XBOOLE_0:def 3; :: thesis: verum

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 <> {} ) )
;

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;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