let X be non empty set ; :: thesis: for R being RMembership_Func of X,X holds (TrCl R) (#) (TrCl R) = "\/" { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } ,(FuzzyLattice [:X,X:])
let R be RMembership_Func of X,X; :: thesis: (TrCl R) (#) (TrCl R) = "\/" { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } ,(FuzzyLattice [:X,X:])
set Q = { (n iter R) where n is Element of NAT : n > 0 } ;
set FL = FuzzyLattice [:X,X:];
A1: "\/" { (n iter R) where n is Element of NAT : n > 0 } ,(FuzzyLattice [:X,X:]) = @ ("\/" { (n iter R) where n is Element of NAT : n > 0 } ,(FuzzyLattice [:X,X:])) by LFUZZY_0:def 5;
A2: { (n iter R) where n is Element of NAT : n > 0 } c= the carrier of (FuzzyLattice [:X,X:])

proof

let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in { (n iter R) where n is Element of NAT : n > 0 } or q in the carrier of (FuzzyLattice [:X,X:]) )
assume q in { (n iter R) where n is Element of NAT : n > 0 } ; :: thesis: q in the carrier of (FuzzyLattice [:X,X:])
then consider i being Element of NAT such that
A3: ( q = i iter R & i > 0 ) ;
[:X,X:],(i iter R) @ = i iter R by LFUZZY_0:def 6;
hence q in the carrier of (FuzzyLattice [:X,X:]) by A3; :: thesis: verum

end;

A4: { ((@ r) (#) (TrCl R)) where r is Element of (FuzzyLattice [:X,X:]) : r in { (n iter R) where n is Element of NAT : n > 0 } } = { ("\/" { ((@ r') (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:])) where r' is Element of (FuzzyLattice [:X,X:]) : r' in { (n iter R) where n is Element of NAT : n > 0 } }

proof

set A = { ((@ r) (#) (TrCl R)) where r is Element of (FuzzyLattice [:X,X:]) : r in { (n iter R) where n is Element of NAT : n > 0 } } ;
set B = { ("\/" { ((@ r') (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:])) where r' is Element of (FuzzyLattice [:X,X:]) : r' in { (n iter R) where n is Element of NAT : n > 0 } } ;
thus { ((@ r) (#) (TrCl R)) where r is Element of (FuzzyLattice [:X,X:]) : r in { (n iter R) where n is Element of NAT : n > 0 } } c= { ("\/" { ((@ r') (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:])) where r' is Element of (FuzzyLattice [:X,X:]) : r' in { (n iter R) where n is Element of NAT : n > 0 } } :: according to XBOOLE_0:def 10 :: thesis: { ("\/" { ((@ r') (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:])) where r' is Element of (FuzzyLattice [:X,X:]) : r' in { (n iter R) where n is Element of NAT : n > 0 } } c= { ((@ r) (#) (TrCl R)) where r is Element of (FuzzyLattice [:X,X:]) : r in { (n iter R) where n is Element of NAT : n > 0 } }

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { ((@ r) (#) (TrCl R)) where r is Element of (FuzzyLattice [:X,X:]) : r in { (n iter R) where n is Element of NAT : n > 0 } } or a in { ("\/" { ((@ r') (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:])) where r' is Element of (FuzzyLattice [:X,X:]) : r' in { (n iter R) where n is Element of NAT : n > 0 } } )
assume a in { ((@ r) (#) (TrCl R)) where r is Element of (FuzzyLattice [:X,X:]) : r in { (n iter R) where n is Element of NAT : n > 0 } } ; :: thesis: a in { ("\/" { ((@ r') (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:])) where r' is Element of (FuzzyLattice [:X,X:]) : r' in { (n iter R) where n is Element of NAT : n > 0 } }
then consider r being Element of (FuzzyLattice [:X,X:]) such that
A5: ( a = (@ r) (#) (TrCl R) & r in { (n iter R) where n is Element of NAT : n > 0 } ) ;
a = "\/" { ((@ r) (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:]) by A1, A2, A5, Th34;
hence a in { ("\/" { ((@ r') (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:])) where r' is Element of (FuzzyLattice [:X,X:]) : r' in { (n iter R) where n is Element of NAT : n > 0 } } by A5; :: thesis: verum

end;

thus { ("\/" { ((@ r') (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:])) where r' is Element of (FuzzyLattice [:X,X:]) : r' in { (n iter R) where n is Element of NAT : n > 0 } } c= { ((@ r) (#) (TrCl R)) where r is Element of (FuzzyLattice [:X,X:]) : r in { (n iter R) where n is Element of NAT : n > 0 } } :: thesis: verum

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { ("\/" { ((@ r') (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:])) where r' is Element of (FuzzyLattice [:X,X:]) : r' in { (n iter R) where n is Element of NAT : n > 0 } } or a in { ((@ r) (#) (TrCl R)) where r is Element of (FuzzyLattice [:X,X:]) : r in { (n iter R) where n is Element of NAT : n > 0 } } )
assume a in { ("\/" { ((@ r') (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:])) where r' is Element of (FuzzyLattice [:X,X:]) : r' in { (n iter R) where n is Element of NAT : n > 0 } } ; :: thesis: a in { ((@ r) (#) (TrCl R)) where r is Element of (FuzzyLattice [:X,X:]) : r in { (n iter R) where n is Element of NAT : n > 0 } }
then consider r being Element of (FuzzyLattice [:X,X:]) such that
A6: ( a = "\/" { ((@ r) (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:]) & r in { (n iter R) where n is Element of NAT : n > 0 } ) ;
a = (@ r) (#) (TrCl R) by A1, A2, A6, Th34;
hence a in { ((@ r) (#) (TrCl R)) where r is Element of (FuzzyLattice [:X,X:]) : r in { (n iter R) where n is Element of NAT : n > 0 } } by A6; :: thesis: verum

end;

end;

A7: { ((@ r) (#) (@ s)) where r, s is Element of (FuzzyLattice [:X,X:]) : ( r in { (n iter R) where n is Element of NAT : n > 0 } & s in { (n iter R) where n is Element of NAT : n > 0 } ) } = { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) }

proof

set A = { ((@ r) (#) (@ s)) where r, s is Element of (FuzzyLattice [:X,X:]) : ( r in { (n iter R) where n is Element of NAT : n > 0 } & s in { (n iter R) where n is Element of NAT : n > 0 } ) } ;
set B = { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } ;
thus { ((@ r) (#) (@ s)) where r, s is Element of (FuzzyLattice [:X,X:]) : ( r in { (n iter R) where n is Element of NAT : n > 0 } & s in { (n iter R) where n is Element of NAT : n > 0 } ) } c= { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } :: according to XBOOLE_0:def 10 :: thesis: { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } c= { ((@ r) (#) (@ s)) where r, s is Element of (FuzzyLattice [:X,X:]) : ( r in { (n iter R) where n is Element of NAT : n > 0 } & s in { (n iter R) where n is Element of NAT : n > 0 } ) }

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { ((@ r) (#) (@ s)) where r, s is Element of (FuzzyLattice [:X,X:]) : ( r in { (n iter R) where n is Element of NAT : n > 0 } & s in { (n iter R) where n is Element of NAT : n > 0 } ) } or a in { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } )
assume a in { ((@ r) (#) (@ s)) where r, s is Element of (FuzzyLattice [:X,X:]) : ( r in { (n iter R) where n is Element of NAT : n > 0 } & s in { (n iter R) where n is Element of NAT : n > 0 } ) } ; :: thesis: a in { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) }
then consider r, s being Element of (FuzzyLattice [:X,X:]) such that
A8: ( a = (@ r) (#) (@ s) & r in { (n iter R) where n is Element of NAT : n > 0 } & s in { (n iter R) where n is Element of NAT : n > 0 } ) ;
consider i being Element of NAT such that
A9: ( r = i iter R & i > 0 ) by A8;
consider j being Element of NAT such that
A10: ( s = j iter R & j > 0 ) by A8;
( r = @ r & s = @ s ) by LFUZZY_0:def 5;
hence a in { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } by A8, A9, A10; :: thesis: verum

end;

thus { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } c= { ((@ r) (#) (@ s)) where r, s is Element of (FuzzyLattice [:X,X:]) : ( r in { (n iter R) where n is Element of NAT : n > 0 } & s in { (n iter R) where n is Element of NAT : n > 0 } ) } :: thesis: verum

proof

let b be set ; :: according to TARSKI:def 3 :: thesis: ( not b in { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } or b in { ((@ r) (#) (@ s)) where r, s is Element of (FuzzyLattice [:X,X:]) : ( r in { (n iter R) where n is Element of NAT : n > 0 } & s in { (n iter R) where n is Element of NAT : n > 0 } ) } )
assume b in { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } ; :: thesis: b in { ((@ r) (#) (@ s)) where r, s is Element of (FuzzyLattice [:X,X:]) : ( r in { (n iter R) where n is Element of NAT : n > 0 } & s in { (n iter R) where n is Element of NAT : n > 0 } ) }
then consider i, j being Element of NAT such that
A11: ( b = (i iter R) (#) (j iter R) & i > 0 & j > 0 ) ;
A12: ( i iter R in { (n iter R) where n is Element of NAT : n > 0 } & j iter R in { (n iter R) where n is Element of NAT : n > 0 } ) by A11;
A13: ( i iter R = [:X,X:],(i iter R) @ & j iter R = [:X,X:],(j iter R) @ ) by LFUZZY_0:def 6;
then reconsider r = i iter R as Element of (FuzzyLattice [:X,X:]) ;
reconsider s = j iter R as Element of (FuzzyLattice [:X,X:]) by A13;
( @ r = r & @ s = s ) by LFUZZY_0:def 5;
hence b in { ((@ r) (#) (@ s)) where r, s is Element of (FuzzyLattice [:X,X:]) : ( r in { (n iter R) where n is Element of NAT : n > 0 } & s in { (n iter R) where n is Element of NAT : n > 0 } ) } by A11, A12; :: thesis: verum

end;

end;

deffunc H₁( Element of (FuzzyLattice [:X,X:]), Element of (FuzzyLattice [:X,X:])) -> Element of the carrier of (FuzzyLattice [:X,X:]) = [:X,X:],((@ $1) (#) (@ $2)) @ ;
defpred S₁[ Element of (FuzzyLattice [:X,X:])] means $1 in { (n iter R) where n is Element of NAT : n > 0 } ;
defpred S₂[ Element of (FuzzyLattice [:X,X:])] means $1 in { (n iter R) where n is Element of NAT : n > 0 } ;
A14: { ("\/" { ((@ r) (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:])) where r is Element of (FuzzyLattice [:X,X:]) : r in { (n iter R) where n is Element of NAT : n > 0 } } = { ("\/" { ([:X,X:],((@ r') (#) (@ s')) @ ) where s' is Element of (FuzzyLattice [:X,X:]) : s' in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:])) where r' is Element of (FuzzyLattice [:X,X:]) : r' in { (n iter R) where n is Element of NAT : n > 0 } }

proof

defpred S₃[ Element of (FuzzyLattice [:X,X:])] means $1 in { (n iter R) where n is Element of NAT : n > 0 } ;
deffunc H₂( Element of (FuzzyLattice [:X,X:])) -> Element of the carrier of (FuzzyLattice [:X,X:]) = "\/" { ((@ $1) (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:]);
deffunc H₃( Element of (FuzzyLattice [:X,X:])) -> Element of the carrier of (FuzzyLattice [:X,X:]) = "\/" { ([:X,X:],((@ $1) (#) (@ s)) @ ) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:]);
for r being Element of (FuzzyLattice [:X,X:]) holds "\/" { ((@ r) (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:]) = "\/" { ([:X,X:],((@ r) (#) (@ s)) @ ) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:])

proof

let r be Element of (FuzzyLattice [:X,X:]); :: thesis: "\/" { ((@ r) (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:]) = "\/" { ([:X,X:],((@ r) (#) (@ s)) @ ) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:])
{ ((@ r) (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } = { ([:X,X:],((@ r) (#) (@ s)) @ ) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } }

proof

defpred S₄[ Element of (FuzzyLattice [:X,X:])] means $1 in { (n iter R) where n is Element of NAT : n > 0 } ;
deffunc H₄( Element of (FuzzyLattice [:X,X:])) -> Element of bool [:[:X,X:],REAL :] = (@ r) (#) (@ $1);
deffunc H₅( Element of (FuzzyLattice [:X,X:])) -> Element of the carrier of (FuzzyLattice [:X,X:]) = [:X,X:],((@ r) (#) (@ $1)) @ ;
A15: for s being Element of (FuzzyLattice [:X,X:]) holds H₄(s) = H₅(s) by LFUZZY_0:def 6;
{ H₄(s) where s is Element of (FuzzyLattice [:X,X:]) : S₄[s] } = { H₅(s) where s is Element of (FuzzyLattice [:X,X:]) : S₄[s] } from FRAENKEL:sch 5(A15);
hence { ((@ r) (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } = { ([:X,X:],((@ r) (#) (@ s)) @ ) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ; :: thesis: verum

end;

hence "\/" { ((@ r) (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:]) = "\/" { ([:X,X:],((@ r) (#) (@ s)) @ ) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:]) ; :: thesis: verum

end;

then A16: for r being Element of (FuzzyLattice [:X,X:]) holds H₂(r) = H₃(r) ;
{ 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 5(A16);
hence { ("\/" { ((@ r) (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:])) where r is Element of (FuzzyLattice [:X,X:]) : r in { (n iter R) where n is Element of NAT : n > 0 } } = { ("\/" { ([:X,X:],((@ r') (#) (@ s')) @ ) where s' is Element of (FuzzyLattice [:X,X:]) : s' in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:])) where r' is Element of (FuzzyLattice [:X,X:]) : r' in { (n iter R) where n is Element of NAT : n > 0 } } ; :: thesis: verum

end;

A17: { ([:X,X:],((@ r) (#) (@ s)) @ ) where r, s is Element of (FuzzyLattice [:X,X:]) : ( r in { (n iter R) where n is Element of NAT : n > 0 } & s in { (n iter R) where n is Element of NAT : n > 0 } ) } = { ((@ r) (#) (@ s)) where r, s is Element of (FuzzyLattice [:X,X:]) : ( r in { (n iter R) where n is Element of NAT : n > 0 } & s in { (n iter R) where n is Element of NAT : n > 0 } ) }

proof

defpred S₃[ Element of (FuzzyLattice [:X,X:]), Element of (FuzzyLattice [:X,X:])] means ( $1 in { (n iter R) where n is Element of NAT : n > 0 } & $2 in { (n iter R) where n is Element of NAT : n > 0 } );
deffunc H₂( Element of (FuzzyLattice [:X,X:]), Element of (FuzzyLattice [:X,X:])) -> Element of the carrier of (FuzzyLattice [:X,X:]) = [:X,X:],((@ $1) (#) (@ $2)) @ ;
deffunc H₃( Element of (FuzzyLattice [:X,X:]), Element of (FuzzyLattice [:X,X:])) -> Element of bool [:[:X,X:],REAL :] = (@ $1) (#) (@ $2);
A18: for r, s being Element of (FuzzyLattice [:X,X:]) holds H₂(r,s) = H₃(r,s) by LFUZZY_0:def 6;
{ H₂(r,s) where r, s is Element of (FuzzyLattice [:X,X:]) : S₃[r,s] } = { H₃(r,s) where r, s is Element of (FuzzyLattice [:X,X:]) : S₃[r,s] } from FRAENKEL:sch 7(A18);
hence { ([:X,X:],((@ r) (#) (@ s)) @ ) where r, s is Element of (FuzzyLattice [:X,X:]) : ( r in { (n iter R) where n is Element of NAT : n > 0 } & s in { (n iter R) where n is Element of NAT : n > 0 } ) } = { ((@ r) (#) (@ s)) where r, s is Element of (FuzzyLattice [:X,X:]) : ( r in { (n iter R) where n is Element of NAT : n > 0 } & s in { (n iter R) where n is Element of NAT : n > 0 } ) } ; :: thesis: verum

end;

thus (TrCl R) (#) (TrCl R) = "\/" { ("\/" { H₁(r,s) where s is Element of (FuzzyLattice [:X,X:]) : S₂[s] } ,(FuzzyLattice [:X,X:])) where r is Element of (FuzzyLattice [:X,X:]) : S₁[r] } ,(FuzzyLattice [:X,X:]) by A1, A2, A4, A14, Th35
.= "\/" { H₁(r,s) where r, s is Element of (FuzzyLattice [:X,X:]) : ( S₁[r] & S₂[s] ) } ,(FuzzyLattice [:X,X:]) from LFUZZY_0:sch 1()
.= "\/" { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } ,(FuzzyLattice [:X,X:]) by A7, A17 ; :: thesis: verum