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

proof

let a be set ; :: 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;

then reconsider F = {the carrier of T} as Subset-Family 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 )
A1: [#] T = the carrier of T ;
thus F is Cover of T :: thesis: F is open

proof

thus the carrier of T c= union F by ZFMISC_1:31; :: according to SETFAM_1:def 12 :: thesis: verum

end;

let P be Subset of T; :: according to TOPS_2:def 1 :: thesis: ( not P in F or P is open )
thus ( not P in F or P is open ) by A1, TARSKI:def 1; :: thesis: verum