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 ;
A1: for p, q being Element of L st p in F & q in F holds
p "/\" q in F ;
for p, q being Element of L st p in F & q in F holds
p "\/" q in F ;
hence the carrier of L is ClosedSubset of L by A1, LATTICES:def 24, LATTICES:def 25; :: thesis: verum