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 & 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: { (((@ ("\/" 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

defpred S₁[ Element of X] means verum;
deffunc H₁( Element of X) -> Element of the carrier of (RealPoset [.0 ,1.]) = ((@ ("\/" Q,(FuzzyLattice [:X,X:]))) . [x,$1]) "/\" (R . [$1,z]);
deffunc H₂( Element of X) -> Element of the carrier of (RealPoset [.0 ,1.]) = ("\/" (pi Q,[x,$1]),(RealPoset [.0 ,1.])) "/\" (R . [$1,z]);
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 A4: 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(A4); :: thesis: verum

end;

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

proof

defpred S₁[ Element of X] means verum;
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.]) = "\/" { (b "/\" (R . [$1,z])) where b is Element of (RealPoset [.0 ,1.]) : b in pi Q,[x,$1] } ,(RealPoset [.0 ,1.]);
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

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.])
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.]))) ;
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 A6: for y being Element of X holds H₁(y) = H₂(y) ;
{ H₁(y) where y is Element of X : S₁[y] } = { H₂(y') where y' is Element of X : S₁[y'] } from FRAENKEL:sch 5(A6);
hence { (("\/" (pi Q,[x,y]),(RealPoset [.0 ,1.])) "/\" (R . [y,z])) where y is Element of X : verum } = { ("\/" { (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 } ; :: thesis: verum

end;

A7: { ("\/" { (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,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 }

proof

defpred S₁[ Element of X] means verum;
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.]) = "\/" { ((r . [x,$1]) "/\" (R . [$1,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(RealPoset [.0 ,1.]);
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 } ;
{ (b "/\" (R . [y,z])) where b is Element of (RealPoset [.0 ,1.]) : b in pi Q,[x,y] } = { ((r . [x,y]) "/\" (R . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q }

proof

thus { (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 } :: according to XBOOLE_0:def 10 :: thesis: { ((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 { (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
A8: ( a = b "/\" (R . [y,z]) & b in pi Q,[x,y] ) ;
consider f being Function such that
A9: ( f in Q & b = f . [x,y] ) by A8, CARD_3:def 6;
thus a in { ((r . [x,y]) "/\" (R . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } by A8, A9; :: thesis: verum

end;

thus { ((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] } :: thesis: verum

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
A10: ( a = (r . [x,y]) "/\" (R . [y,z]) & r in Q ) ;
r . [x,y] in pi Q,[x,y] by A10, 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 A10; :: thesis: verum

end;

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.]) ; :: 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.]) = "\/" { ("\/" { ((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.])

proof

defpred S₁[ Element of X] means verum;
defpred S₂[ Element of (FuzzyLattice [:X,X:])] means $1 in Q;
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]);
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₂(y',r') where y' is Element of X : S₁[y'] } ,(RealPoset [.0 ,1.])) where r' is Element of (FuzzyLattice [:X,X:]) : S₂[r'] } ,(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 } = { ("\/" { (((@ 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 }

proof

defpred S₁[ Element of (FuzzyLattice [:X,X:])] means $1 in Q;
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.]);
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

defpred S₂[ Element of X] means verum;
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]);
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) . [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 } = { (((@ r') (#) R) . [x,z]) where r' is Element of (FuzzyLattice [:X,X:]) : r' in Q }

proof

defpred S₁[ Element of (FuzzyLattice [:X,X:])] means $1 in Q;
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) (#) R) . [x,z];
A18: 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(A18); :: thesis: verum

end;

A19: { (((@ 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
A20: ( a = ((@ r) (#) R) . [x,z] & r in Q ) ;
(@ r) (#) R in { ((@ r') (#) R) where r' is Element of (FuzzyLattice [:X,X:]) : r' in Q } by A20;
hence a in pi { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z] by A20, 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
A21: ( f in { ((@ r') (#) R) where r' is Element of (FuzzyLattice [:X,X:]) : r' in Q } & b = f . [x,z] ) by CARD_3:def 6;
consider r being Element of (FuzzyLattice [:X,X:]) such that
A22: ( f = (@ r) (#) R & r in Q ) by A21;
thus b in { (((@ r) (#) R) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } by A21, A22; :: thesis: verum

end;

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, A3, A5, A7, A12, A14, A17, A19, 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