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

proof

the carrier of ET is open Subset of ET

proof

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

proof

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;

hence the carrier of ET is open Subset of ET by Def1; :: thesis: verum

end;

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

end;

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

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;

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