let X be non empty set ; :: thesis: for R being RMembership_Func of X,X
for Q being Subset of (FuzzyLattice [:X,X:])
for x, z being Element of X holds { ((R . x,y) "/\" ((@ ("\/" Q,(FuzzyLattice [:X,X:]))) . y,z)) where y is Element of X : verum } = { ((R . [x,y]) "/\" ("\/" (pi Q,[y,z]),(RealPoset [.0 ,1.]))) where y is Element of X : verum }
let R be RMembership_Func of X,X; :: thesis: for Q being Subset of (FuzzyLattice [:X,X:])
for x, z being Element of X holds { ((R . x,y) "/\" ((@ ("\/" Q,(FuzzyLattice [:X,X:]))) . y,z)) where y is Element of X : verum } = { ((R . [x,y]) "/\" ("\/" (pi Q,[y,z]),(RealPoset [.0 ,1.]))) where y is Element of X : verum }
let Q be Subset of (FuzzyLattice [:X,X:]); :: thesis: for x, z being Element of X holds { ((R . x,y) "/\" ((@ ("\/" Q,(FuzzyLattice [:X,X:]))) . y,z)) where y is Element of X : verum } = { ((R . [x,y]) "/\" ("\/" (pi Q,[y,z]),(RealPoset [.0 ,1.]))) where y is Element of X : verum }
let x, z be Element of X; :: thesis: { ((R . x,y) "/\" ((@ ("\/" Q,(FuzzyLattice [:X,X:]))) . y,z)) where y is Element of X : verum } = { ((R . [x,y]) "/\" ("\/" (pi Q,[y,z]),(RealPoset [.0 ,1.]))) where y is Element of X : verum }
defpred S₁[ Element of X] means verum;
deffunc H₁( Element of X) -> Element of the carrier of (RealPoset [.0 ,1.]) = (R . x,$1) "/\" ((@ ("\/" Q,(FuzzyLattice [:X,X:]))) . $1,z);
deffunc H₂( Element of X) -> Element of the carrier of (RealPoset [.0 ,1.]) = (R . [x,$1]) "/\" ("\/" (pi Q,[$1,z]),(RealPoset [.0 ,1.]));
for y being Element of X holds (R . [x,y]) "/\" ((@ ("\/" Q,(FuzzyLattice [:X,X:]))) . [y,z]) = (R . [x,y]) "/\" ("\/" (pi Q,[y,z]),(RealPoset [.0 ,1.]))

proof

let y be Element of X; :: thesis: (R . [x,y]) "/\" ((@ ("\/" Q,(FuzzyLattice [:X,X:]))) . [y,z]) = (R . [x,y]) "/\" ("\/" (pi Q,[y,z]),(RealPoset [.0 ,1.]))
(@ ("\/" Q,(FuzzyLattice [:X,X:]))) . [y,z] = ("\/" Q,(FuzzyLattice [:X,X:])) . [y,z] by LFUZZY_0:def 5
.= "\/" (pi Q,[y,z]),(RealPoset [.0 ,1.]) by Th32 ;
hence (R . [x,y]) "/\" ((@ ("\/" Q,(FuzzyLattice [:X,X:]))) . [y,z]) = (R . [x,y]) "/\" ("\/" (pi Q,[y,z]),(RealPoset [.0 ,1.])) ; :: thesis: verum

end;

then A1: for y being Element of X holds H₁(y) = H₂(y) ;
thus { H₁(y) where y is Element of X : S₁[y] } = { H₂(y9) where y9 is Element of X : S₁[y9] } from FRAENKEL:sch 5(A1); :: thesis: verum