let S be non empty full join-inheriting SubRelStr of L; S is with_suprema
now for x, y being Element of S holds ex_sup_of {x,y},Slet x,
y be
Element of
S;
ex_sup_of {x,y},Sreconsider 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;
verum end;
hence
S is with_suprema
by Th20; verum