let S be non empty full meet-inheriting SubRelStr of L; S is with_infima
now for x, y being Element of S holds ex_inf_of {x,y},Slet x,
y be
Element of
S;
ex_inf_of {x,y},Sreconsider 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;
verum end;
hence
S is with_infima
by Th21; verum