theorem :: WAYBEL23:24

for L being non empty transitive RelStr
for S being non empty join-closed Subset of L
for x, y being Element of S st ex_sup_of {x,y},L holds
( ex_sup_of {x,y}, subrelstr S & "\/" ({x,y},(subrelstr S)) = "\/" ({x,y},L) )