let L be non empty transitive RelStr ; :: thesis: 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 )
let S be non empty join-closed Subset of L; :: thesis: 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 )
let x, y be Element of S; :: thesis: ( ex_sup_of {x,y},L implies ( ex_sup_of {x,y}, subrelstr S & "\/" {x,y},(subrelstr S) = "\/" {x,y},L ) )
A1: subrelstr S is non empty full join-inheriting SubRelStr of L by Def2;
A2: ( x is Element of (subrelstr S) & y is Element of (subrelstr S) ) by YELLOW_0:def 15;
assume A3: ex_sup_of {x,y},L ; :: thesis: ( ex_sup_of {x,y}, subrelstr S & "\/" {x,y},(subrelstr S) = "\/" {x,y},L )
then "\/" {x,y},L in the carrier of (subrelstr S) by A1, A2, YELLOW_0:def 17;
hence ( ex_sup_of {x,y}, subrelstr S & "\/" {x,y},(subrelstr S) = "\/" {x,y},L ) by A2, A3, YELLOW_0:67; :: thesis: verum