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

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