let ET be FMT_TopSpace; :: thesis: ( {} in Family_open_set ET & the carrier of ET in Family_open_set ET & ( for a being Subset-Family of ET st a c= Family_open_set ET holds
union a in Family_open_set ET ) & ( for a, b being Subset of ET st a in Family_open_set ET & b in Family_open_set ET holds
a /\ b in Family_open_set ET ) )
A1: ET is U_FMT_filter ;
thus {} in Family_open_set ET :: thesis: ( the carrier of ET in Family_open_set ET & ( for a being Subset-Family of ET st a c= Family_open_set ET holds
union a in Family_open_set ET ) & ( for a, b being Subset of ET st a in Family_open_set ET & b in Family_open_set ET holds
a /\ b in Family_open_set ET ) )

proof

set S = {} ;
{} c= the carrier of ET ;
then reconsider S = {} as Subset of ET ;
S is open ;
then reconsider S = S as open Subset of ET ;
S in { O where O is open Subset of ET : verum } ;
hence {} in Family_open_set ET ; :: thesis: verum

end;

thus the carrier of ET in Family_open_set ET :: thesis: ( ( for a being Subset-Family of ET st a c= Family_open_set ET holds
union a in Family_open_set ET ) & ( for a, b being Subset of ET st a in Family_open_set ET & b in Family_open_set ET holds
a /\ b in Family_open_set ET ) )

proof

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 A1;
hence S in U_FMT x by CARD_FIL:5; :: thesis: verum

end;

then S is open ;
then reconsider S = S as open Subset of ET ;
S in { O where O is open Subset of ET : verum } ;
hence the carrier of ET in Family_open_set ET ; :: thesis: verum

end;

thus for a being Subset-Family of ET st a c= Family_open_set ET holds
union a in Family_open_set ET :: thesis: for a, b being Subset of ET st a in Family_open_set ET & b in Family_open_set ET holds
a /\ b in Family_open_set ET

proof

let a be Subset-Family of ET; :: thesis: ( a c= Family_open_set ET implies union a in Family_open_set ET )
assume A2: a c= Family_open_set ET ; :: thesis: union a in Family_open_set ET
reconsider UA = union a as Subset of ET ;

now :: thesis: for x being Element of ET st x in UA holds
UA in U_FMT x

let x be Element of ET; :: thesis: ( x in UA implies UA in U_FMT x )
assume x in UA ; :: thesis: UA in U_FMT x
then consider Y being set such that
A3: x in Y and
A4: Y in a by TARSKI:def 4;
Y in { O where O is open Subset of ET : verum } by A2, A4;
then consider Y0 being open Subset of ET such that
A5: Y = Y0 ;
A6: Y in U_FMT x by A3, A5, Def1;
A7: Y c= UA by A4, ZFMISC_1:74;
U_FMT x is Filter of the carrier of ET by A1;
hence UA in U_FMT x by A6, A7, CARD_FIL:def 1; :: thesis: verum

end;

then UA is open ;
hence union a in Family_open_set ET ; :: thesis: verum

end;

thus for a, b being Subset of ET st a in Family_open_set ET & b in Family_open_set ET holds
a /\ b in Family_open_set ET :: thesis: verum

proof

let a, b be Subset of ET; :: thesis: ( a in Family_open_set ET & b in Family_open_set ET implies a /\ b in Family_open_set ET )
assume that
A9: a in Family_open_set ET and
A10: b in Family_open_set ET ; :: thesis: a /\ b in Family_open_set ET

now :: thesis: for x being Element of ET st x in a /\ b holds
a /\ b in U_FMT x

let x be Element of ET; :: thesis: ( x in a /\ b implies a /\ b in U_FMT x )
assume A11: x in a /\ b ; :: thesis: a /\ b in U_FMT x
A12: ( x in a & x in b ) by A11, XBOOLE_0:def 4;
consider a0 being open Subset of ET such that
A13: a = a0 by A9;
A14: a in U_FMT x by A12, A13, Def1;
consider b0 being open Subset of ET such that
A15: b = b0 by A10;
A16: b in U_FMT x by A12, A15, Def1;
U_FMT x is Filter of the carrier of ET by A1;
hence a /\ b in U_FMT x by A14, A16, CARD_FIL:def 1; :: thesis: verum

end;

then a /\ b is open ;
then reconsider AB = a /\ b as open Subset of ET ;
AB in { O where O is open Subset of ET : verum } ;
hence a /\ b in Family_open_set ET ; :: thesis: verum

end;