let T be complete LATTICE; :: thesis: for S being non empty full SubRelStr of T st S is infs-inheriting holds
S is complete
let S be non empty full SubRelStr of T; :: thesis: ( S is infs-inheriting implies S is complete )
assume A1: S is infs-inheriting ; :: thesis: S is complete
now :: thesis: for X being set holds ex_inf_of X,S
let X be set ; :: thesis: ex_inf_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_inf_of Y,T by YELLOW_0:17;
then "/\" (Y,T) in the carrier of S by A1;
then ex_inf_of Y,S by A2, YELLOW_0:63;
hence ex_inf_of X,S by YELLOW_0:50; :: thesis: verum
end;
hence S is complete by YELLOW_2:25; :: thesis: verum