set FF = { F where F is Subset of FT : ( A c= F & F is closed ) } ;

{ F where F is Subset of FT : ( A c= F & F is closed ) } c= bool the carrier of FT

meet FF is Subset of FT ;

hence meet { F where F is Subset of FT : ( A c= F & F is closed ) } is Subset of FT ; :: thesis: verum

{ F where F is Subset of FT : ( A c= F & F is closed ) } c= bool the carrier of FT

proof

then reconsider FF = { F where F is Subset of FT : ( A c= F & F is closed ) } as Subset-Family of FT ;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { F where F is Subset of FT : ( A c= F & F is closed ) } or x in bool the carrier of FT )

assume x in { F where F is Subset of FT : ( A c= F & F is closed ) } ; :: thesis: x in bool the carrier of FT

then ex F being Subset of FT st

( x = F & A c= F & F is closed ) ;

hence x in bool the carrier of FT ; :: thesis: verum

end;assume x in { F where F is Subset of FT : ( A c= F & F is closed ) } ; :: thesis: x in bool the carrier of FT

then ex F being Subset of FT st

( x = F & A c= F & F is closed ) ;

hence x in bool the carrier of FT ; :: thesis: verum

meet FF is Subset of FT ;

hence meet { F where F is Subset of FT : ( A c= F & F is closed ) } is Subset of FT ; :: thesis: verum