:: deftheorem Def17 defines join-inheriting YELLOW_0:def 17 :
for L being non empty RelStr
for S being SubRelStr of L holds
( S is join-inheriting iff for x, y being Element of L st x in the carrier of S & y in the carrier of S & ex_sup_of {x,y},L holds
sup {x,y} in the carrier of S );