:: deftheorem defines @ LFUZZY_0:def 5 :
for X being non empty set
for a being Element of (FuzzyLattice X) holds @ a = a;