for L1, L2 being RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds
for X being Subset of L1
for Y being Subset of L2 st X = Y holds
( downarrow X = downarrow Y & uparrow X = uparrow Y )