:: deftheorem defines ex_max_of WAYBEL_1:def 5 :
for S being non empty RelStr
for X being set holds
( ex_max_of X,S iff ( ex_sup_of X,S & "\/" (X,S) in X ) );