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 ) )

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 ) )

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

a /\ b in Family_open_set ET :: thesis: verum

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

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
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;{} 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

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

thus
for a being Subset-Family of ET st a c= Family_open_set ET holds
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

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;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

then
S is open
;
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;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

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

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

thus
for a, b being Subset of ET st a in Family_open_set ET & b in Family_open_set ET holds
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 ;

hence union a in Family_open_set ET ; :: thesis: verum

end;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

then
UA is open
;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;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

hence union a in Family_open_set ET ; :: thesis: verum

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

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;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

then
a /\ b is open
;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;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

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