let X be non empty set ; :: thesis: for R being RMembership_Func of X,X
for Q being Subset of (FuzzyLattice [:X,X:]) holds (@ ("\/" Q,(FuzzyLattice [:X,X:]))) (#) R = "\/" { ((@ 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 (@ ("\/" Q,(FuzzyLattice [:X,X:]))) (#) R = "\/" { ((@ 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: (@ ("\/" Q,(FuzzyLattice [:X,X:]))) (#) R = "\/" { ((@ 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 ((@ ("\/" Q,(FuzzyLattice [:X,X:]))) (#) R) . x,z = F . x,z

proof

let x, z be Element of X; :: thesis: ((@ ("\/" Q,(FuzzyLattice [:X,X:]))) (#) R) . 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 set ; :: 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;

A3: { (("\/" (pi Q,[x,y]),(RealPoset [.0 ,1.])) "/\" (R . [y,z])) where y is Element of X : verum } = { ("\/" { (b "/\" (R . [y9,z])) where b is Element of (RealPoset [.0 ,1.]) : b in pi Q,[x,y9] } ,(RealPoset [.0 ,1.])) where y9 is Element of X : verum }

proof

deffunc H₁( Element of X) -> Element of the carrier of (RealPoset [.0 ,1.]) = "\/" { (b "/\" (R . [$1,z])) where b is Element of (RealPoset [.0 ,1.]) : b in pi Q,[x,$1] } ,(RealPoset [.0 ,1.]);
deffunc H₂( Element of X) -> Element of the carrier of (RealPoset [.0 ,1.]) = ("\/" (pi Q,[x,$1]),(RealPoset [.0 ,1.])) "/\" (R . [$1,z]);
defpred S₁[ Element of X] means verum;
for y being Element of X holds ("\/" (pi Q,[x,y]),(RealPoset [.0 ,1.])) "/\" (R . [y,z]) = "\/" { (b "/\" (R . [y,z])) where b is Element of (RealPoset [.0 ,1.]) : b in pi Q,[x,y] } ,(RealPoset [.0 ,1.])

proof

FuzzyLattice [:X,X:] = (RealPoset [.0 ,1.]) |^ [:X,X:] by LFUZZY_0:def 4
.= product ([:X,X:] --> (RealPoset [.0 ,1.])) by YELLOW_1:def 5 ;
then reconsider Q = Q as Subset of (product ([:X,X:] --> (RealPoset [.0 ,1.]))) ;
let y be Element of X; :: thesis: ("\/" (pi Q,[x,y]),(RealPoset [.0 ,1.])) "/\" (R . [y,z]) = "\/" { (b "/\" (R . [y,z])) where b is Element of (RealPoset [.0 ,1.]) : b in pi Q,[x,y] } ,(RealPoset [.0 ,1.])
pi Q,[x,y] is Subset of (RealPoset [.0 ,1.]) by FUNCOP_1:13;
hence ("\/" (pi Q,[x,y]),(RealPoset [.0 ,1.])) "/\" (R . [y,z]) = "\/" { (b "/\" (R . [y,z])) where b is Element of (RealPoset [.0 ,1.]) : b in pi Q,[x,y] } ,(RealPoset [.0 ,1.]) by LFUZZY_0:15; :: thesis: verum

end;

then A4: for y being Element of X holds H₂(y) = H₁(y) ;
{ H₂(y) where y is Element of X : S₁[y] } = { H₁(y9) where y9 is Element of X : S₁[y9] } from FRAENKEL:sch 5(A4);
hence { (("\/" (pi Q,[x,y]),(RealPoset [.0 ,1.])) "/\" (R . [y,z])) where y is Element of X : verum } = { ("\/" { (b "/\" (R . [y9,z])) where b is Element of (RealPoset [.0 ,1.]) : b in pi Q,[x,y9] } ,(RealPoset [.0 ,1.])) where y9 is Element of X : verum } ; :: thesis: verum

end;

A5: { ("\/" { (b "/\" (R . [y,z])) where b is Element of (RealPoset [.0 ,1.]) : b in pi Q,[x,y] } ,(RealPoset [.0 ,1.])) where y is Element of X : verum } = { ("\/" { ((r . [x,y9]) "/\" (R . [y9,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(RealPoset [.0 ,1.])) where y9 is Element of X : verum }

proof

deffunc H₁( Element of X) -> Element of the carrier of (RealPoset [.0 ,1.]) = "\/" { ((r . [x,$1]) "/\" (R . [$1,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(RealPoset [.0 ,1.]);
deffunc H₂( Element of X) -> Element of the carrier of (RealPoset [.0 ,1.]) = "\/" { (b "/\" (R . [$1,z])) where b is Element of (RealPoset [.0 ,1.]) : b in pi Q,[x,$1] } ,(RealPoset [.0 ,1.]);
defpred S₁[ Element of X] means verum;
for y being Element of X holds "\/" { (b "/\" (R . [y,z])) where b is Element of (RealPoset [.0 ,1.]) : b in pi Q,[x,y] } ,(RealPoset [.0 ,1.]) = "\/" { ((r . [x,y]) "/\" (R . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(RealPoset [.0 ,1.])

proof

let y be Element of X; :: thesis: "\/" { (b "/\" (R . [y,z])) where b is Element of (RealPoset [.0 ,1.]) : b in pi Q,[x,y] } ,(RealPoset [.0 ,1.]) = "\/" { ((r . [x,y]) "/\" (R . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(RealPoset [.0 ,1.])
set A = { (b "/\" (R . [y,z])) where b is Element of (RealPoset [.0 ,1.]) : b in pi Q,[x,y] } ;
set B = { ((r . [x,y]) "/\" (R . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ;
A6: { ((r . [x,y]) "/\" (R . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } c= { (b "/\" (R . [y,z])) where b is Element of (RealPoset [.0 ,1.]) : b in pi Q,[x,y] }

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { ((r . [x,y]) "/\" (R . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } or a in { (b "/\" (R . [y,z])) where b is Element of (RealPoset [.0 ,1.]) : b in pi Q,[x,y] } )
assume a in { ((r . [x,y]) "/\" (R . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ; :: thesis: a in { (b "/\" (R . [y,z])) where b is Element of (RealPoset [.0 ,1.]) : b in pi Q,[x,y] }
then consider r being Element of (FuzzyLattice [:X,X:]) such that
A7: a = (r . [x,y]) "/\" (R . [y,z]) and
A8: r in Q ;
r . [x,y] in pi Q,[x,y] by A8, CARD_3:def 6;
hence a in { (b "/\" (R . [y,z])) where b is Element of (RealPoset [.0 ,1.]) : b in pi Q,[x,y] } by A7; :: thesis: verum

end;

{ (b "/\" (R . [y,z])) where b is Element of (RealPoset [.0 ,1.]) : b in pi Q,[x,y] } c= { ((r . [x,y]) "/\" (R . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q }

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { (b "/\" (R . [y,z])) where b is Element of (RealPoset [.0 ,1.]) : b in pi Q,[x,y] } or a in { ((r . [x,y]) "/\" (R . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } )
assume a in { (b "/\" (R . [y,z])) where b is Element of (RealPoset [.0 ,1.]) : b in pi Q,[x,y] } ; :: thesis: a in { ((r . [x,y]) "/\" (R . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q }
then consider b being Element of (RealPoset [.0 ,1.]) such that
A9: a = b "/\" (R . [y,z]) and
A10: b in pi Q,[x,y] ;
ex f being Function st
( f in Q & b = f . [x,y] ) by A10, CARD_3:def 6;
hence a in { ((r . [x,y]) "/\" (R . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } by A9; :: thesis: verum

end;

hence "\/" { (b "/\" (R . [y,z])) where b is Element of (RealPoset [.0 ,1.]) : b in pi Q,[x,y] } ,(RealPoset [.0 ,1.]) = "\/" { ((r . [x,y]) "/\" (R . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(RealPoset [.0 ,1.]) by A6, XBOOLE_0:def 10; :: thesis: verum

end;

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

end;

A12: "\/" { ("\/" { ((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.]) = "\/" { ("\/" { ((r9 . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } ,(RealPoset [.0 ,1.])) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in Q } ,(RealPoset [.0 ,1.])

proof

deffunc H₁( Element of X, Element of (FuzzyLattice [:X,X:])) -> Element of the carrier of (RealPoset [.0 ,1.]) = ($2 . [x,$1]) "/\" (R . [$1,z]);
deffunc H₂( Element of X, Element of (FuzzyLattice [:X,X:])) -> Element of the carrier of (RealPoset [.0 ,1.]) = ($2 . [x,$1]) "/\" (R . [$1,z]);
defpred S₁[ Element of (FuzzyLattice [:X,X:])] means $1 in Q;
defpred S₂[ Element of X] means verum;
A13: for y being Element of X
for r being Element of (FuzzyLattice [:X,X:]) st S₂[y] & S₁[r] holds
H₂(y,r) = H₁(y,r) ;
thus "\/" { ("\/" { H₂(y,r) where r is Element of (FuzzyLattice [:X,X:]) : S₁[r] } ,(RealPoset [.0 ,1.])) where y is Element of X : S₂[y] } ,(RealPoset [.0 ,1.]) = "\/" { ("\/" { H₁(y9,r9) where y9 is Element of X : S₂[y9] } ,(RealPoset [.0 ,1.])) where r9 is Element of (FuzzyLattice [:X,X:]) : S₁[r9] } ,(RealPoset [.0 ,1.]) from LFUZZY_0:sch 5(A13); :: thesis: verum

end;

A14: { ("\/" { ((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 } = { ("\/" { (((@ r9) . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } ,(RealPoset [.0 ,1.])) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in Q }

proof

deffunc H₁( Element of (FuzzyLattice [:X,X:])) -> Element of the carrier of (RealPoset [.0 ,1.]) = "\/" { (((@ $1) . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } ,(RealPoset [.0 ,1.]);
deffunc H₂( Element of (FuzzyLattice [:X,X:])) -> Element of the carrier of (RealPoset [.0 ,1.]) = "\/" { (($1 . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } ,(RealPoset [.0 ,1.]);
defpred S₁[ Element of (FuzzyLattice [:X,X:])] means $1 in Q;
for r being Element of (FuzzyLattice [:X,X:]) st r in Q holds
"\/" { ((r . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } ,(RealPoset [.0 ,1.]) = "\/" { (((@ r) . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } ,(RealPoset [.0 ,1.])

proof

let r be Element of (FuzzyLattice [:X,X:]); :: thesis: ( r in Q implies "\/" { ((r . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } ,(RealPoset [.0 ,1.]) = "\/" { (((@ r) . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } ,(RealPoset [.0 ,1.]) )
assume r in Q ; :: thesis: "\/" { ((r . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } ,(RealPoset [.0 ,1.]) = "\/" { (((@ r) . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } ,(RealPoset [.0 ,1.])
{ ((r . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } = { (((@ r) . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum }

proof

deffunc H₃( Element of X) -> Element of the carrier of (RealPoset [.0 ,1.]) = ((@ r) . [x,$1]) "/\" (R . [$1,z]);
deffunc H₄( Element of X) -> Element of the carrier of (RealPoset [.0 ,1.]) = (r . [x,$1]) "/\" (R . [$1,z]);
defpred S₂[ Element of X] means verum;
A15: for y being Element of X holds H₄(y) = H₃(y) by LFUZZY_0:def 5;
thus { H₄(y) where y is Element of X : S₂[y] } = { H₃(y) where y is Element of X : S₂[y] } from FRAENKEL:sch 5(A15); :: thesis: verum

end;

hence "\/" { ((r . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } ,(RealPoset [.0 ,1.]) = "\/" { (((@ r) . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } ,(RealPoset [.0 ,1.]) ; :: thesis: verum

end;

then A16: for r being Element of (FuzzyLattice [:X,X:]) st S₁[r] holds
H₂(r) = H₁(r) ;
thus { H₂(r) where r is Element of (FuzzyLattice [:X,X:]) : S₁[r] } = { H₁(r) where r is Element of (FuzzyLattice [:X,X:]) : S₁[r] } from FRAENKEL:sch 6(A16); :: thesis: verum

end;

A17: { (((@ r) (#) R) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } = pi { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z]

proof

set A = { (((@ r) (#) R) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ;
set B = pi { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z];
thus { (((@ r) (#) R) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } c= pi { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z] :: according to XBOOLE_0:def 10 :: thesis: pi { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z] c= { (((@ r) (#) R) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q }

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { (((@ r) (#) R) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } or a in pi { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z] )
assume a in { (((@ r) (#) R) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ; :: thesis: a in pi { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z]
then consider r being Element of (FuzzyLattice [:X,X:]) such that
A18: a = ((@ r) (#) R) . [x,z] and
A19: r in Q ;
(@ r) (#) R in { ((@ r9) (#) R) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in Q } by A19;
hence a in pi { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z] by A18, CARD_3:def 6; :: thesis: verum

end;

thus pi { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z] c= { (((@ r) (#) R) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } :: thesis: verum

proof

let b be set ; :: according to TARSKI:def 3 :: thesis: ( not b in pi { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z] or b in { (((@ r) (#) R) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } )
assume b in pi { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z] ; :: thesis: b in { (((@ r) (#) R) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q }
then consider f being Function such that
A20: f in { ((@ r9) (#) R) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in Q } and
A21: b = f . [x,z] by CARD_3:def 6;
ex r being Element of (FuzzyLattice [:X,X:]) st
( f = (@ r) (#) R & r in Q ) by A20;
hence b in { (((@ r) (#) R) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } by A21; :: thesis: verum

end;

end;

A22: { (((@ ("\/" Q,(FuzzyLattice [:X,X:]))) . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } = { (("\/" (pi Q,[x,y]),(RealPoset [.0 ,1.])) "/\" (R . [y,z])) where y is Element of X : verum }

proof

deffunc H₁( Element of X) -> Element of the carrier of (RealPoset [.0 ,1.]) = ("\/" (pi Q,[x,$1]),(RealPoset [.0 ,1.])) "/\" (R . [$1,z]);
deffunc H₂( Element of X) -> Element of the carrier of (RealPoset [.0 ,1.]) = ((@ ("\/" Q,(FuzzyLattice [:X,X:]))) . [x,$1]) "/\" (R . [$1,z]);
defpred S₁[ Element of X] means verum;
for y being Element of X holds ((@ ("\/" Q,(FuzzyLattice [:X,X:]))) . [x,y]) "/\" (R . [y,z]) = ("\/" (pi Q,[x,y]),(RealPoset [.0 ,1.])) "/\" (R . [y,z])

proof

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

end;

then A23: 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(A23); :: thesis: verum

end;

A24: { ("\/" { (((@ 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 } = { (((@ r9) (#) R) . [x,z]) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in Q }

proof

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

end;

thus ((@ ("\/" Q,(FuzzyLattice [:X,X:]))) (#) R) . x,z = "\/" { (((@ ("\/" Q,(FuzzyLattice [:X,X:]))) . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } ,(RealPoset [.0 ,1.]) by Lm6
.= F . x,z by A1, A22, A3, A5, A12, A14, A24, A17, Th32 ; :: thesis: verum

end;

hence (@ ("\/" Q,(FuzzyLattice [:X,X:]))) (#) R = "\/" { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(FuzzyLattice [:X,X:]) by Th2; :: thesis: verum