:: deftheorem Def15 defines latt LATTICE3:def 15 :
for A being RelStr st A is with_suprema with_infima Poset holds
for b₂ being strict Lattice holds
( b₂ = latt A iff RelStr(# the carrier of A, the InternalRel of A #) = LattPOSet b₂ );