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

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, YELLOW_0:def 19;
then ex_sup_of Y,S by A2, YELLOW_0:65;
hence ex_sup_of X,S by YELLOW_0:50; :: thesis: verum

end;

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