theorem Th19: :: LATWAL_2:31

for A being WA-Lattice ex L being strict WA_Lattice st RelStr(# the carrier of A, the InternalRel of A #) = LatRelStr L