set OO = { O where O is open Subset of ET : verum } ;

A1: not { O where O is open Subset of ET : verum } is empty

hence { O where O is open Subset of ET : verum } is non empty Subset-Family of the carrier of ET by A1; :: thesis: verum

A1: not { O where O is open Subset of ET : verum } is empty

proof

the carrier of ET is open Subset of ET

hence not { O where O is open Subset of ET : verum } is empty ; :: thesis: verum

end;proof

then
the carrier of ET in { O where O is open Subset of ET : verum }
;
A2:
ET is U_FMT_filter
;

set S = the carrier of ET;

the carrier of ET c= the carrier of ET ;

then reconsider S = the carrier of ET as Subset of ET ;

for x being Element of ET st x in S holds

S in U_FMT x

end;set S = the carrier of ET;

the carrier of ET c= the carrier of ET ;

then reconsider S = the carrier of ET as Subset of ET ;

for x being Element of ET st x in S holds

S in U_FMT x

proof

hence
the carrier of ET is open Subset of ET
by Def1; :: thesis: verum
let x be Element of ET; :: thesis: ( x in S implies S in U_FMT x )

assume x in S ; :: thesis: S in U_FMT x

U_FMT x is Filter of the carrier of ET by A2;

hence S in U_FMT x by CARD_FIL:5; :: thesis: verum

end;assume x in S ; :: thesis: S in U_FMT x

U_FMT x is Filter of the carrier of ET by A2;

hence S in U_FMT x by CARD_FIL:5; :: thesis: verum

hence not { O where O is open Subset of ET : verum } is empty ; :: thesis: verum

now :: thesis: for t being object st t in { O where O is open Subset of ET : verum } holds

t in bool the carrier of ET

then
{ O where O is open Subset of ET : verum } c= bool the carrier of ET
;t in bool the carrier of ET

let t be object ; :: thesis: ( t in { O where O is open Subset of ET : verum } implies t in bool the carrier of ET )

assume t in { O where O is open Subset of ET : verum } ; :: thesis: t in bool the carrier of ET

then consider OO1 being open Subset of ET such that

A3: t = OO1 ;

thus t in bool the carrier of ET by A3; :: thesis: verum

end;assume t in { O where O is open Subset of ET : verum } ; :: thesis: t in bool the carrier of ET

then consider OO1 being open Subset of ET such that

A3: t = OO1 ;

thus t in bool the carrier of ET by A3; :: thesis: verum

hence { O where O is open Subset of ET : verum } is non empty Subset-Family of the carrier of ET by A1; :: thesis: verum