let A be non empty set ; :: thesis: the carrier of (FuzzyLattice A) = Funcs (A,[.0,1.])
thus the carrier of (FuzzyLattice A) = Funcs (A, the carrier of (RealPoset [.0,1.])) by YELLOW_1:28
.= Funcs (A,[.0,1.]) by Def3 ; :: thesis: verum