let L be Lattice; :: thesis: the carrier of L is ClosedSubset of L
the carrier of L c= the carrier of L ;
then reconsider F = the carrier of L as Subset of L ;
for p, q being Element of L st p in F & q in F holds
( p "/\" q in F & p "\/" q in F ) ;
hence the carrier of L is ClosedSubset of L by Def10; :: thesis: verum