:: deftheorem defines inherits_sup_of YELLOW16:def 6 :
for S, T being non empty RelStr
for X being set holds
( S inherits_sup_of X,T iff ( ex_sup_of X,T implies "\/" (X,T) in the carrier of S ) );