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_sup_of {x,y}, FuzzyLattice [.0,1.] holds
sup {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_sup_of {x,y}, FuzzyLattice [.0,1.] implies sup {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_sup_of {x,y}, FuzzyLattice [.0,1.] ) ; :: thesis: sup {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 = sup {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 = max ((@ x),(@ y)) by LFUZZY_0:19
.= max (xx,yy) by MaxEqMax ;
fxy is Fuzzy_Negation by F1, T3, YELLOW_0:41;
then fxy in { f where f is Fuzzy_Negation : verum } ;
hence sup {x,y} in the carrier of Fuzzy_Negations by F1, FuzNegDef; :: thesis: verum

end;

hence Fuzzy_Negations is join-inheriting by YELLOW_0:def 17; :: thesis: verum