:: deftheorem defines LattPOSet LATTICE3:def 2 :
for L being Lattice holds LattPOSet L = RelStr(# the carrier of L,(LattRel L) #);