:: deftheorem Def13 defines sup CLASSES5:def 12 :
for U1, U2 being Universe holds
( ( U2 in U1 implies sup (U1,U2) = U1 ) & ( not U2 in U1 implies sup (U1,U2) = U2 ) );