theorem :: WAYBEL_0:25

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 X1 being Subset of L1
for X2 being Subset of L2 st X1 = X2 holds
( ( X1 is lower implies X2 is lower ) & ( X1 is upper implies X2 is upper ) )