let X be non empty set ; :: thesis: for R being RMembership_Func of X,X
for Q being Subset of
for x, z being Element of X holds { ("\/" { ((R . [x,y]) "/\" ((@ r) . [y,z])) where y is Element of X : verum } ,(RealPoset [.0 ,1.])) where r is Element of : r in Q } = { ((R (#) (@ r)) . [x,z]) where r is Element of : r in Q }
let R be RMembership_Func of X,X; :: thesis: for Q being Subset of
for x, z being Element of X holds { ("\/" { ((R . [x,y]) "/\" ((@ r) . [y,z])) where y is Element of X : verum } ,(RealPoset [.0 ,1.])) where r is Element of : r in Q } = { ((R (#) (@ r)) . [x,z]) where r is Element of : r in Q }
let Q be Subset of ; :: thesis: for x, z being Element of X holds { ("\/" { ((R . [x,y]) "/\" ((@ r) . [y,z])) where y is Element of X : verum } ,(RealPoset [.0 ,1.])) where r is Element of : r in Q } = { ((R (#) (@ r)) . [x,z]) where r is Element of : r in Q }
let x, z be Element of X; :: thesis: { ("\/" { ((R . [x,y]) "/\" ((@ r) . [y,z])) where y is Element of X : verum } ,(RealPoset [.0 ,1.])) where r is Element of : r in Q } = { ((R (#) (@ r)) . [x,z]) where r is Element of : r in Q }
set FL = FuzzyLattice [:X,X:];
defpred S₁[ Element of ] means $1 in Q;
deffunc H₁( Element of ) -> Element of the carrier of (RealPoset [.0 ,1.]) = "\/" { ((R . [x,y]) "/\" ((@ $1) . [y,z])) where y is Element of X : verum } ,(RealPoset [.0 ,1.]);
deffunc H₂( Element of ) -> Element of the carrier of (RealPoset [.0 ,1.]) = (R (#) (@ $1)) . [x,z];
A1: for r being Element of st S₁[r] holds
H₁(r) = H₂(r) by Lm6;
thus { H₁(r) where r is Element of : S₁[r] } = { H₂(r) where r is Element of : S₁[r] } from FRAENKEL:sch 6(A1); :: thesis: verum