let L be non empty RelStr ; :: thesis: for S being Subset of L holds
( S is join-closed iff for x, y being Element of L st x in S & y in S & ex_sup_of {x,y},L holds
sup {x,y} in S )

let S be Subset of L; :: thesis: ( S is join-closed iff for x, y being Element of L st x in S & y in S & ex_sup_of {x,y},L holds
sup {x,y} in S )

thus ( S is join-closed implies for x, y being Element of L st x in S & y in S & ex_sup_of {x,y},L holds
sup {x,y} in S ) :: thesis: ( ( for x, y being Element of L st x in S & y in S & ex_sup_of {x,y},L holds
sup {x,y} in S ) implies S is join-closed )
proof
assume S is join-closed ; :: thesis: for x, y being Element of L st x in S & y in S & ex_sup_of {x,y},L holds
sup {x,y} in S

then A1: subrelstr S is join-inheriting ;
let x, y be Element of L; :: thesis: ( x in S & y in S & ex_sup_of {x,y},L implies sup {x,y} in S )
assume that
A2: x in S and
A3: y in S and
A4: ex_sup_of {x,y},L ; :: thesis: sup {x,y} in S
the carrier of () = S by YELLOW_0:def 15;
hence sup {x,y} in S by A1, A2, A3, A4; :: thesis: verum
end;
assume A5: for x, y being Element of L st x in S & y in S & ex_sup_of {x,y},L holds
sup {x,y} in S ; :: thesis: S is join-closed
now :: thesis: for x, y being Element of L st x in the carrier of () & y in the carrier of () & ex_sup_of {x,y},L holds
sup {x,y} in the carrier of ()
let x, y be Element of L; :: thesis: ( x in the carrier of () & y in the carrier of () & ex_sup_of {x,y},L implies sup {x,y} in the carrier of () )
assume that
A6: x in the carrier of () and
A7: y in the carrier of () and
A8: ex_sup_of {x,y},L ; :: thesis: sup {x,y} in the carrier of ()
the carrier of () = S by YELLOW_0:def 15;
hence sup {x,y} in the carrier of () by A5, A6, A7, A8; :: thesis: verum
end;
then subrelstr S is join-inheriting ;
hence S is join-closed ; :: thesis: verum