let X be non empty set ; :: thesis: for R being RMembership_Func of X,X
for Q being Subset of (FuzzyLattice [:X,X:]) holds R (#) (@ ("\/" (Q,(FuzzyLattice [:X,X:])))) = "\/" ( { (R (#) (@ r)) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(FuzzyLattice [:X,X:]))
let R be RMembership_Func of X,X; :: thesis: for Q being Subset of (FuzzyLattice [:X,X:]) holds R (#) (@ ("\/" (Q,(FuzzyLattice [:X,X:])))) = "\/" ( { (R (#) (@ r)) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(FuzzyLattice [:X,X:]))
let Q be Subset of (FuzzyLattice [:X,X:]); :: thesis: R (#) (@ ("\/" (Q,(FuzzyLattice [:X,X:])))) = "\/" ( { (R (#) (@ r)) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(FuzzyLattice [:X,X:]))
set FL = FuzzyLattice [:X,X:];
set RP = RealPoset [.0,1.];
"\/" ( { (R (#) (@ r)) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(FuzzyLattice [:X,X:])) = @ ("\/" ( { (R (#) (@ r)) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(FuzzyLattice [:X,X:]))) by LFUZZY_0:def 5;
then reconsider F = "\/" ( { (R (#) (@ r)) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(FuzzyLattice [:X,X:])) as RMembership_Func of X,X ;
for x, z being Element of X holds (R (#) (@ ("\/" (Q,(FuzzyLattice [:X,X:]))))) . (x,z) = F . (x,z)
proof
let x, z be Element of X; :: thesis: (R (#) (@ ("\/" (Q,(FuzzyLattice [:X,X:]))))) . (x,z) = F . (x,z)
A1: { (R (#) (@ r)) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } c= the carrier of (FuzzyLattice [:X,X:])
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in { (R (#) (@ r)) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } or t in the carrier of (FuzzyLattice [:X,X:]) )
assume t in { (R (#) (@ r)) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ; :: thesis: t in the carrier of (FuzzyLattice [:X,X:])
then consider r being Element of (FuzzyLattice [:X,X:]) such that
A2: t = R (#) (@ r) and
r in Q ;
([:X,X:],(R (#) (@ r))) @ = R (#) (@ r) by LFUZZY_0:def 6;
hence t in the carrier of (FuzzyLattice [:X,X:]) by A2; :: thesis: verum
end;
thus (R (#) (@ ("\/" (Q,(FuzzyLattice [:X,X:]))))) . (x,z) = "\/" ( { ((R . (x,y)) "/\" ((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) . (y,z))) where y is Element of X : verum } ,(RealPoset [.0,1.])) by LFUZZY_0:22
.= "\/" ( { ((R . [x,y]) "/\" ("\/" ((pi (Q,[y,z])),(RealPoset [.0,1.])))) where y is Element of X : verum } ,(RealPoset [.0,1.])) by Lm2
.= "\/" ( { ("\/" ( { ((R . [x,y]) "/\" b) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[y,z]) } ,(RealPoset [.0,1.]))) where y is Element of X : verum } ,(RealPoset [.0,1.])) by Lm3
.= "\/" ( { ("\/" ( { ((R . [x,y]) "/\" (r . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(RealPoset [.0,1.]))) where y is Element of X : verum } ,(RealPoset [.0,1.])) by Lm4
.= "\/" ( { ("\/" ( { ((R . [x,y]) "/\" (r . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.]))) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(RealPoset [.0,1.])) by Lm10
.= "\/" ( { ("\/" ( { ((R . [x,y]) "/\" ((@ r) . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.]))) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(RealPoset [.0,1.])) by Lm7
.= "\/" ( { ((R (#) (@ r)) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(RealPoset [.0,1.])) by Lm8
.= "\/" ((pi ( { (R (#) (@ r)) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z])),(RealPoset [.0,1.])) by Lm9
.= F . (x,z) by A1, Th32 ; :: thesis: verum
end;
hence R (#) (@ ("\/" (Q,(FuzzyLattice [:X,X:])))) = "\/" ( { (R (#) (@ r)) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(FuzzyLattice [:X,X:])) by Th2; :: thesis: verum