:: deftheorem defines FuzzyLattice LFUZZY_0:def 4 :
for A being non empty set holds FuzzyLattice A = (RealPoset [.0,1.]) |^ A;