let T be TopSpace; :: thesis: ex F being Subset-Family of T st

( F = { the carrier of T} & F is Cover of T & F is open )

set F = { the carrier of T};

{ the carrier of T} c= bool the carrier of T

take F ; :: thesis: ( F = { the carrier of T} & F is Cover of T & F is open )

thus F = { the carrier of T} ; :: thesis: ( F is Cover of T & F is open )

the carrier of T c= union F by ZFMISC_1:25;

hence F is Cover of T by SETFAM_1:def 11; :: thesis: F is open

let P be Subset of T; :: according to TOPS_2:def 1 :: thesis: ( not P in F or P is open )

[#] T = the carrier of T ;

hence ( not P in F or P is open ) by TARSKI:def 1; :: thesis: verum

( F = { the carrier of T} & F is Cover of T & F is open )

set F = { the carrier of T};

{ the carrier of T} c= bool the carrier of T

proof

then reconsider F = { the carrier of T} as Subset-Family of T ;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { the carrier of T} or a in bool the carrier of T )

assume a in { the carrier of T} ; :: thesis: a in bool the carrier of T

then a = the carrier of T by TARSKI:def 1;

hence a in bool the carrier of T by ZFMISC_1:def 1; :: thesis: verum

end;assume a in { the carrier of T} ; :: thesis: a in bool the carrier of T

then a = the carrier of T by TARSKI:def 1;

hence a in bool the carrier of T by ZFMISC_1:def 1; :: thesis: verum

take F ; :: thesis: ( F = { the carrier of T} & F is Cover of T & F is open )

thus F = { the carrier of T} ; :: thesis: ( F is Cover of T & F is open )

the carrier of T c= union F by ZFMISC_1:25;

hence F is Cover of T by SETFAM_1:def 11; :: thesis: F is open

let P be Subset of T; :: according to TOPS_2:def 1 :: thesis: ( not P in F or P is open )

[#] T = the carrier of T ;

hence ( not P in F or P is open ) by TARSKI:def 1; :: thesis: verum