theorem Th16: :: WAYBEL29:16

for L1, L2 being non empty up-complete Poset st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds
Sigma L1 = Sigma L2