let L be complete LATTICE; :: thesis: for S being non empty full sups-inheriting SubRelStr of L holds S is complete LATTICE
let S be non empty full sups-inheriting SubRelStr of L; :: thesis: S is complete LATTICE
for X being Subset of S holds ex_sup_of X,S

proof

let X be Subset of S; :: thesis: ex_sup_of X,S
A1: ex_sup_of X,L by YELLOW_0:17;
then "\/" (X,L) in the carrier of S by YELLOW_0:def 19;
hence ex_sup_of X,S by A1, YELLOW_0:64; :: thesis: verum

end;

then S is complete by YELLOW_0:53;
hence S is complete LATTICE ; :: thesis: verum