let S be non empty full meet-inheriting SubRelStr of L; :: thesis: S is with_infima
now let x,
y be
Element of
S;
:: thesis: ex_inf_of {x,y},Sreconsider a =
x,
b =
y as
Element of
L by Th59;
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, Th64;
:: thesis: verum end;
hence
S is with_infima
by Th21; :: thesis: verum