set L = FuzzyLattice [.0,1.];
set S = Fuzzy_Negations ;
for x, y being Element of (FuzzyLattice [.0,1.]) st x in the carrier of Fuzzy_Negations & y in the carrier of Fuzzy_Negations & ex_inf_of {x,y}, FuzzyLattice [.0,1.] holds
inf {x,y} in the carrier of Fuzzy_Negations

proof

let x, y be Element of (FuzzyLattice [.0,1.]); :: thesis: ( x in the carrier of Fuzzy_Negations & y in the carrier of Fuzzy_Negations & ex_inf_of {x,y}, FuzzyLattice [.0,1.] implies inf {x,y} in the carrier of Fuzzy_Negations )
assume S0: ( x in the carrier of Fuzzy_Negations & y in the carrier of Fuzzy_Negations & ex_inf_of {x,y}, FuzzyLattice [.0,1.] ) ; :: thesis: inf {x,y} in the carrier of Fuzzy_Negations
then x in { f where f is Fuzzy_Negation : verum } by FuzNegDef;
then consider f being Fuzzy_Negation such that
S1: x = f ;
y in { f where f is Fuzzy_Negation : verum } by S0, FuzNegDef;
then consider g being Fuzzy_Negation such that
s1: y = g ;
reconsider xx = x, yy = y as Fuzzy_Negation by S1, s1;
consider fxy being Function such that
F1: ( fxy = inf {x,y} & dom fxy = [.0,1.] & rng fxy c= [.0,1.] ) by FUNCT_2:def 2, LemmaCarrier;
reconsider fxy = fxy as UnOp of [.0,1.] by F1, FUNCT_2:2;
T3: x "/\" y = min ((@ x),(@ y)) by LFUZZY_0:21
.= min (xx,yy) by MinEqMin ;
fxy is Fuzzy_Negation by F1, T3, YELLOW_0:40;
then fxy in { f where f is Fuzzy_Negation : verum } ;
hence inf {x,y} in the carrier of Fuzzy_Negations by F1, FuzNegDef; :: thesis: verum

end;

hence Fuzzy_Negations is meet-inheriting by YELLOW_0:def 16; :: thesis: verum