theorem Th5: :: WAYBEL13:5

for L1 being non empty reflexive antisymmetric lower-bounded RelStr
for L2 being non empty reflexive antisymmetric RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is up-complete holds
the carrier of (CompactSublatt L1) = the carrier of (CompactSublatt L2)