theorem :: LFUZZY_0:17

for C being non empty set
for s, t being Element of (FuzzyLattice C) holds
( s <<= t iff for c being Element of C holds (@ s) . c <= (@ t) . c )