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 set holds
( ( ex_sup_of X,L1 implies ex_sup_of X,L2 ) & ( ex_inf_of X,L1 implies ex_inf_of X,L2 ) )