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

proof

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

end;

then S is complete by Th28;
hence S is complete LATTICE ; :: thesis: verum