let S be non empty full join-inheriting SubRelStr of L; :: thesis: S is with_suprema

now :: thesis: for x, y being Element of S holds ex_sup_of {x,y},S

let x, y be Element of S; :: thesis: ex_sup_of {x,y},S
reconsider a = x, b = y as Element of L by Th58;
A1: ex_sup_of {a,b},L by Th20;
then "\/" ({a,b},L) in the carrier of S by Def17;
hence ex_sup_of {x,y},S by A1, Th64; :: thesis: verum

end;

hence S is with_suprema by Th20; :: thesis: verum