for S, T being non empty antisymmetric RelStr
for x, y being Element of [:S,T:] holds
( ex_sup_of {x,y},[:S,T:] iff ( ex_sup_of {(x `1),(y `1)},S & ex_sup_of {(x `2),(y `2)},T ) )