theorem :: WAYBEL20:11

for L1, L2, T1, T2 being non empty antisymmetric RelStr
for f being Function of L1,T1
for g being Function of L2,T2 st f is sups-preserving & g is sups-preserving holds
[:f,g:] is sups-preserving