set X = { f where f is Fuzzy_Negation : verum } ;
reconsider X = { f where f is Fuzzy_Negation : verum } as Subset of (FuzzyLattice [.0,1.]) by LemmaCarrier, LemmaFuncs;
the carrier of (subrelstr X) = X by YELLOW_0:def 15;
hence ex b₁ being strict full SubRelStr of FuzzyLattice [.0,1.] st the carrier of b₁ = { f where f is Fuzzy_Negation : verum } ; :: thesis: verum