let S be non empty full meet-inheriting SubRelStr of L; :: thesis: S is with_infima

now :: thesis: for x, y being Element of S holds ex_inf_of {x,y},S

let x, y be Element of S; :: thesis: ex_inf_of {x,y},S
reconsider a = x, b = y as Element of L by Th58;
A1: ex_inf_of {a,b},L by Th21;
then "/\" ({a,b},L) in the carrier of S by Def16;
hence ex_inf_of {x,y},S by A1, Th63; :: thesis: verum

end;

hence S is with_infima by Th21; :: thesis: verum