let T be complete LATTICE; :: thesis: for S being non empty full SubRelStr of T st S is sups-inheriting holds
S is complete
let S be non empty full SubRelStr of T; :: thesis: ( S is sups-inheriting implies S is complete )
assume A1: S is sups-inheriting ; :: thesis: S is complete

now :: thesis: for X being set holds ex_sup_of X,S

let X be set ; :: thesis: ex_sup_of X,S
set Y = X /\ the carrier of S;
reconsider Y = X /\ the carrier of S as Subset of S by XBOOLE_1:17;
A2: ex_sup_of Y,T by YELLOW_0:17;
then "\/" (Y,T) in the carrier of S by A1;
then ex_sup_of Y,S by A2, YELLOW_0:64;
hence ex_sup_of X,S by YELLOW_0:50; :: thesis: verum

end;

hence S is complete by YELLOW_2:24; :: thesis: verum