let C be non empty set ; :: thesis: for s, t being Element of (FuzzyLattice C) holds

( s <<= t iff for c being Element of C holds (@ s) . c <= (@ t) . c )

let s, t be Element of (FuzzyLattice C); :: thesis: ( s <<= t iff for c being Element of C holds (@ s) . c <= (@ t) . c )

( (C,(@ s)) @ = s & (C,(@ t)) @ = t ) ;

hence ( s <<= t iff for c being Element of C holds (@ s) . c <= (@ t) . c ) by Th16; :: thesis: verum

( s <<= t iff for c being Element of C holds (@ s) . c <= (@ t) . c )

let s, t be Element of (FuzzyLattice C); :: thesis: ( s <<= t iff for c being Element of C holds (@ s) . c <= (@ t) . c )

( (C,(@ s)) @ = s & (C,(@ t)) @ = t ) ;

hence ( s <<= t iff for c being Element of C holds (@ s) . c <= (@ t) . c ) by Th16; :: thesis: verum