:: LFUZZY_0 semantic presentation

begin

definition
let R be RelStr ;
attrR is real  means :Def1: :: LFUZZY_0:def 1
( the carrier of R c= REAL & ( for x, y being real number st x in the carrier of R & y in the carrier of R holds
( [x,y] in the InternalRel of R iff x <= y ) ) );
end;

:: deftheorem Def1 defines real LFUZZY_0:def_1_:_
 for R being RelStr holds
( R is real iff ( the carrier of R c= REAL & ( for x, y being real number st x in the carrier of R & y in the carrier of R holds
( [x,y] in the InternalRel of R iff x <= y ) ) ) );

definition
let R be RelStr ;
attrR is interval  means :Def2: :: LFUZZY_0:def 2
( R is real & ex a, b being real number st
( a <= b & the carrier of R = [.a,b.] ) );
end;

:: deftheorem Def2 defines interval LFUZZY_0:def_2_:_
 for R being RelStr holds
( R is interval iff ( R is real & ex a, b being real number st
( a <= b & the carrier of R = [.a,b.] ) ) );

registration
cluster interval  ->  non empty real for RelStr ;
coherence
 for b1 being RelStr st b1 is interval holds
( b1 is real & not b1 is empty )
proof
let R be RelStr ; ::_thesis: ( R is interval implies ( R is real & not R is empty ) )
assume A1: R is real ; :: according to LFUZZY_0:def_2 ::_thesis: ( for a, b being real number holds
( not a <= b or not the carrier of R = [.a,b.] ) or ( R is real & not R is empty ) )
given a, b being real number  such that A2: ( a <= b & the carrier of R = [.a,b.] ) ; ::_thesis: ( R is real & not R is empty )
thus  R is real by A1; ::_thesis: not R is empty
thus  not the carrier of R is empty by A2, XXREAL_1:1; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
end;

registration
cluster empty  ->  real for RelStr ;
coherence
 for b1 being RelStr st b1 is empty holds
b1 is real
proof
let R be RelStr ; ::_thesis: ( R is empty implies R is real )
assume A1: the carrier of R is empty ; :: according to STRUCT_0:def_1 ::_thesis: R is real
hence  the carrier of R c= REAL by XBOOLE_1:2; :: according to LFUZZY_0:def_1 ::_thesis: for x, y being real number st x in the carrier of R & y in the carrier of R holds
( [x,y] in the InternalRel of R iff x <= y )
thus  for x, y being real number st x in the carrier of R & y in the carrier of R holds
( [x,y] in the InternalRel of R iff x <= y ) by A1; ::_thesis: verum
end;
end;

theorem Th1: :: LFUZZY_0:1
for X being Subset of REAL ex R being strict RelStr st
( the carrier of R = X & R is real )
proof
let X be Subset of REAL; ::_thesis: ex R being strict RelStr st
( the carrier of R = X & R is real )
percases ( X is empty or not X is empty ) ;
supposeA1: X is empty ; ::_thesis: ex R being strict RelStr st
( the carrier of R = X & R is real )
set E = the empty strict RelStr ;
take  the empty strict RelStr ; ::_thesis: ( the carrier of the empty strict RelStr = X & the empty strict RelStr is real )
thus  ( the carrier of the empty strict RelStr = X & the empty strict RelStr is real ) by A1; ::_thesis: verum
end;
suppose not X is empty ; ::_thesis: ex R being strict RelStr st
( the carrier of R = X & R is real )
then reconsider Y = X as non empty set ;
defpred S1[ set , set ] means  ex x, y being real number st
( $1 = x & $2 = y & x <= y );
consider L being non empty strict RelStr  such that
A2: the carrier of L = Y and
A3: for a, b being Element of L holds
( a <= b iff S1[a,b] ) from YELLOW_0:sch_1();
take  L ; ::_thesis: ( the carrier of L = X & L is real )
thus  the carrier of L = X by A2; ::_thesis: L is real
thus  the carrier of L c= REAL by A2; :: according to LFUZZY_0:def_1 ::_thesis: for x, y being real number st x in the carrier of L & y in the carrier of L holds
( [x,y] in the InternalRel of L iff x <= y )
let x, y be real number ; ::_thesis: ( x in the carrier of L & y in the carrier of L implies ( [x,y] in the InternalRel of L iff x <= y ) )
assume  ( x in the carrier of L & y in the carrier of L ) ; ::_thesis: ( [x,y] in the InternalRel of L iff x <= y )
then reconsider a = x, b = y as Element of L ;
 ( a <= b iff [x,y] in the InternalRel of L ) by ORDERS_2:def_5;
then  ( [x,y] in the InternalRel of L iff ex x, y being real number st
( a = x & b = y & x <= y ) ) by A3;
hence  ( [x,y] in the InternalRel of L iff x <= y ) ; ::_thesis: verum
end;
end;
end;

registration
cluster strict interval for RelStr ;
existence
 ex b1 being RelStr st
( b1 is interval & b1 is strict )
proof
set X = [.0,1.];
consider R being strict RelStr  such that
A1: ( the carrier of R = [.0,1.] & R is real ) by Th1;
take  R ; ::_thesis: ( R is interval & R is strict )
thus  ( R is interval & R is strict ) by A1, Def2; ::_thesis: verum
end;
end;

theorem Th2: :: LFUZZY_0:2
for R1, R2 being real RelStr st the carrier of R1 = the carrier of R2 holds
RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #)
proof
let R1, R2 be real RelStr ; ::_thesis: ( the carrier of R1 = the carrier of R2 implies RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) )
assume A1: the carrier of R1 = the carrier of R2 ; ::_thesis: RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #)
set X = the carrier of R1;
 the InternalRel of R1 = the InternalRel of R2
proof
let a, b be set ; :: according to RELAT_1:def_2 ::_thesis: ( ( not [a,b] in the InternalRel of R1 or [a,b] in the InternalRel of R2 ) & ( not [a,b] in the InternalRel of R2 or [a,b] in the InternalRel of R1 ) )
A2: the carrier of R1 c= REAL by Def1;
hereby  ::_thesis: ( not [a,b] in the InternalRel of R2 or [a,b] in the InternalRel of R1 )
assume A3: [a,b] in the InternalRel of R1 ; ::_thesis: [a,b] in the InternalRel of R2
then A4: ( a in the carrier of R1 & b in the carrier of R1 ) by ZFMISC_1:87;
then reconsider a9 = a, b9 = b as Element of REAL by A2;
 a9 <= b9 by A3, A4, Def1;
hence  [a,b] in the InternalRel of R2 by A1, A4, Def1; ::_thesis: verum
end;
assume A5: [a,b] in the InternalRel of R2 ; ::_thesis: [a,b] in the InternalRel of R1
then A6: ( a in the carrier of R1 & b in the carrier of R1 ) by A1, ZFMISC_1:87;
then reconsider a9 = a, b9 = b as Element of REAL by A2;
 a9 <= b9 by A1, A5, A6, Def1;
hence  [a,b] in the InternalRel of R1 by A6, Def1; ::_thesis: verum
end;
hence  RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) by A1; ::_thesis: verum
end;

registration
let R be non empty real RelStr ;
cluster  ->  real for Element of the carrier of R;
coherence
 for b1 being Element of R holds b1 is real
proof
let x be Element of R; ::_thesis: x is real
 the carrier of R c= REAL by Def1;
hence  x is real ; ::_thesis: verum
end;
end;

definition
let X be Subset of REAL;
func RealPoset X ->  strict real RelStr  means :Def3: :: LFUZZY_0:def 3
 the carrier of it = X;
existence
 ex b1 being strict real RelStr st the carrier of b1 = X
proof
 ex R being strict RelStr st
( the carrier of R = X & R is real ) by Th1;
hence  ex b1 being strict real RelStr st the carrier of b1 = X ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict real RelStr st the carrier of b1 = X & the carrier of b2 = X holds
b1 = b2 by Th2;
end;

:: deftheorem Def3 defines RealPoset LFUZZY_0:def_3_:_
 for X being Subset of REAL
for b2 being strict real RelStr holds
( b2 = RealPoset X iff the carrier of b2 = X );

registration
let X be non empty Subset of REAL;
cluster RealPoset X ->  non empty strict real ;
coherence
 not RealPoset X is empty by Def3;
end;

notation
let R be RelStr ;
let x, y be Element of R;
synonym x <<= y for x <= y;
synonym y >>= x for x <= y;
antonym x ~<= y for x <= y;
antonym y ~>= x for x <= y;
end;

theorem Th3: :: LFUZZY_0:3
for R being non empty real RelStr
for x, y being Element of R holds
( x <= y iff x <<= y )
proof
let R be non empty real RelStr ; ::_thesis: for x, y being Element of R holds
( x <= y iff x <<= y )
let x, y be Element of R; ::_thesis: ( x <= y iff x <<= y )
 ( [x,y] in the InternalRel of R iff x <= y ) by Def1;
hence  ( x <= y iff x <<= y ) by ORDERS_2:def_5; ::_thesis: verum
end;

registration
cluster real  ->  reflexive transitive antisymmetric for RelStr ;
coherence
 for b1 being RelStr st b1 is real holds
( b1 is reflexive & b1 is antisymmetric & b1 is transitive )
proof
let R be RelStr ; ::_thesis: ( R is real implies ( R is reflexive & R is antisymmetric & R is transitive ) )
assume A1: R is real ; ::_thesis: ( R is reflexive & R is antisymmetric & R is transitive )
percases ( R is empty or not R is empty ) ;
suppose R is empty ; ::_thesis: ( R is reflexive & R is antisymmetric & R is transitive )
hence  ( R is reflexive & R is antisymmetric & R is transitive ) ; ::_thesis: verum
end;
suppose not R is empty ; ::_thesis: ( R is reflexive & R is antisymmetric & R is transitive )
then reconsider R9 = R as non empty real RelStr by A1;
A2: R9 is antisymmetric
proof
let x, y be Element of R9; :: according to YELLOW_0:def_3 ::_thesis: ( not x <<= y or not y <<= x or x = y )
assume  ( x <<= y & x >>= y ) ; ::_thesis: x = y
then  ( x <= y & x >= y ) by Th3;
hence  x = y by XXREAL_0:1; ::_thesis: verum
end;
A3: R9 is transitive
proof
let x, y, z be Element of R9; :: according to YELLOW_0:def_2 ::_thesis: ( not x <<= y or not y <<= z or x <<= z )
assume  ( x <<= y & y <<= z ) ; ::_thesis: x <<= z
then  ( x <= y & y <= z ) by Th3;
then  x <= z by XXREAL_0:2;
hence  x <<= z by Th3; ::_thesis: verum
end;
 R9 is reflexive
proof
let x be Element of R9; :: according to YELLOW_0:def_1 ::_thesis: x <<= x
thus  x <<= x by Th3; ::_thesis: verum
end;
hence  ( R is reflexive & R is antisymmetric & R is transitive ) by A2, A3; ::_thesis: verum
end;
end;
end;
end;

registration
cluster non empty real  ->  non empty connected real for RelStr ;
coherence
 for b1 being non empty real RelStr holds b1 is connected
proof
let R be non empty real RelStr ; ::_thesis: R is connected
let x, y be Element of R; :: according to WAYBEL_0:def_29 ::_thesis: ( x <<= y or y <<= x )
 ( x <= y or x >= y ) ;
hence  ( x <<= y or y <<= x ) by Th3; ::_thesis: verum
end;
end;

definition
let R be non empty real RelStr ;
let x, y be Element of R;
:: original: max
redefine func max (x,y) ->  Element of R;
coherence
 max (x,y) is Element of R by XXREAL_0:16;
end;

definition
let R be non empty real RelStr ;
let x, y be Element of R;
:: original: min
redefine func min (x,y) ->  Element of R;
coherence
 min (x,y) is Element of R by XXREAL_0:15;
end;

registration
cluster non empty real  ->  non empty with_suprema with_infima real for RelStr ;
coherence
 for b1 being non empty real RelStr holds
( b1 is with_suprema & b1 is with_infima ) ;
end;


registration
let R be non empty real RelStr ;
let a, b be Element of R;
identifya "\/" b with  max (a,b);
compatibility
 a "\/" b = max (a,b)
proof
A1: for d being Element of R st d >>= a & d >>= b holds
max (a,b) <<= d
proof
let d be Element of R; ::_thesis: ( d >>= a & d >>= b implies max (a,b) <<= d )
assume  ( d >>= a & d >>= b ) ; ::_thesis: max (a,b) <<= d
then  ( d >= a & d >= b ) by Th3;
then  max (a,b) <= d by XXREAL_0:28;
hence  max (a,b) <<= d by Th3; ::_thesis: verum
end;
 max (a,b) >= b by XXREAL_0:25;
then A2: max (a,b) >>= b by Th3;
 max (a,b) >= a by XXREAL_0:25;
then  max (a,b) >>= a by Th3;
hence  a "\/" b = max (a,b) by A2, A1, YELLOW_0:22; ::_thesis: verum
end;
identifya "/\" b with  min (a,b);
compatibility
 a "/\" b = min (a,b)
proof
A3: for d being Element of R st d <<= a & d <<= b holds
min (a,b) >>= d
proof
let d be Element of R; ::_thesis: ( d <<= a & d <<= b implies min (a,b) >>= d )
assume  ( d <<= a & d <<= b ) ; ::_thesis: min (a,b) >>= d
then  ( d <= a & d <= b ) by Th3;
then  d <= min (a,b) by XXREAL_0:20;
hence  min (a,b) >>= d by Th3; ::_thesis: verum
end;
 min (a,b) <= b by XXREAL_0:17;
then A4: min (a,b) <<= b by Th3;
 min (a,b) <= a by XXREAL_0:17;
then  min (a,b) <<= a by Th3;
hence  a "/\" b = min (a,b) by A4, A3, YELLOW_0:23; ::_thesis: verum
end;
end;

theorem :: LFUZZY_0:4
for R being non empty real RelStr
for a, b being Element of R holds a "\/" b = max (a,b) ;

theorem :: LFUZZY_0:5
for R being non empty real RelStr
for a, b being Element of R holds a "/\" b = min (a,b) ;

theorem Th6: :: LFUZZY_0:6
for R being non empty real RelStr holds
( ex x being real number st
( x in the carrier of R & ( for y being real number st y in the carrier of R holds
x <= y ) ) iff R is lower-bounded )
proof
let R be non empty real RelStr ; ::_thesis: ( ex x being real number st
( x in the carrier of R & ( for y being real number st y in the carrier of R holds
x <= y ) ) iff R is lower-bounded )
hereby  ::_thesis: ( R is lower-bounded implies ex x being real number st
( x in the carrier of R & ( for y being real number st y in the carrier of R holds
x <= y ) ) )
given x being real number  such that A1: x in the carrier of R and
A2: for y being real number st y in the carrier of R holds
x <= y ; ::_thesis: R is lower-bounded
reconsider a = x as Element of R by A1;
now__::_thesis:_for_b_being_Element_of_R_st_b_in_the_carrier_of_R_holds_
a_<<=_b
let b be Element of R; ::_thesis: ( b in the carrier of R implies a <<= b )
assume  b in the carrier of R ; ::_thesis: a <<= b
 b >= a by A2;
hence  a <<= b by Th3; ::_thesis: verum
end;
then  a is_<=_than the carrier of R by LATTICE3:def_8;
hence  R is lower-bounded by YELLOW_0:def_4; ::_thesis: verum
end;
given x being Element of R such that A3: x is_<=_than the carrier of R ; :: according to YELLOW_0:def_4 ::_thesis: ex x being real number st
( x in the carrier of R & ( for y being real number st y in the carrier of R holds
x <= y ) )
take  x ; ::_thesis: ( x in the carrier of R & ( for y being real number st y in the carrier of R holds
x <= y ) )
thus  x in the carrier of R ; ::_thesis: for y being real number st y in the carrier of R holds
x <= y
let y be real number ; ::_thesis: ( y in the carrier of R implies x <= y )
assume  y in the carrier of R ; ::_thesis: x <= y
then reconsider b = y as Element of R ;
 x <<= b by A3, LATTICE3:def_8;
hence  x <= y by Th3; ::_thesis: verum
end;

theorem Th7: :: LFUZZY_0:7
for R being non empty real RelStr holds
( ex x being real number st
( x in the carrier of R & ( for y being real number st y in the carrier of R holds
x >= y ) ) iff R is upper-bounded )
proof
let R be non empty real RelStr ; ::_thesis: ( ex x being real number st
( x in the carrier of R & ( for y being real number st y in the carrier of R holds
x >= y ) ) iff R is upper-bounded )
hereby  ::_thesis: ( R is upper-bounded implies ex x being real number st
( x in the carrier of R & ( for y being real number st y in the carrier of R holds
x >= y ) ) )
given x being real number  such that A1: x in the carrier of R and
A2: for y being real number st y in the carrier of R holds
x >= y ; ::_thesis: R is upper-bounded
reconsider a = x as Element of R by A1;
now__::_thesis:_for_b_being_Element_of_R_st_b_in_the_carrier_of_R_holds_
a_>>=_b
let b be Element of R; ::_thesis: ( b in the carrier of R implies a >>= b )
assume  b in the carrier of R ; ::_thesis: a >>= b
 a >= b by A2;
hence  a >>= b by Th3; ::_thesis: verum
end;
then  a is_>=_than the carrier of R by LATTICE3:def_9;
hence  R is upper-bounded by YELLOW_0:def_5; ::_thesis: verum
end;
given x being Element of R such that A3: x is_>=_than the carrier of R ; :: according to YELLOW_0:def_5 ::_thesis: ex x being real number st
( x in the carrier of R & ( for y being real number st y in the carrier of R holds
x >= y ) )
take  x ; ::_thesis: ( x in the carrier of R & ( for y being real number st y in the carrier of R holds
x >= y ) )
thus  x in the carrier of R ; ::_thesis: for y being real number st y in the carrier of R holds
x >= y
let y be real number ; ::_thesis: ( y in the carrier of R implies x >= y )
assume  y in the carrier of R ; ::_thesis: x >= y
then reconsider b = y as Element of R ;
 x >>= b by A3, LATTICE3:def_9;
hence  x >= y by Th3; ::_thesis: verum
end;

registration
cluster non empty interval  ->  non empty bounded for RelStr ;
coherence
 for b1 being non empty RelStr st b1 is interval holds
b1 is bounded
proof
let R be non empty RelStr ; ::_thesis: ( R is interval implies R is bounded )
assume A1: R is real ; :: according to LFUZZY_0:def_2 ::_thesis: ( for a, b being real number holds
( not a <= b or not the carrier of R = [.a,b.] ) or R is bounded )
given x, y being real number  such that A2: x <= y and
A3: the carrier of R = [.x,y.] ; ::_thesis: R is bounded
 ex x being real number st
( x in the carrier of R & ( for y being real number st y in the carrier of R holds
x <= y ) )
proof
take  x ; ::_thesis: ( x in the carrier of R & ( for y being real number st y in the carrier of R holds
x <= y ) )
thus  x in the carrier of R by A2, A3, XXREAL_1:1; ::_thesis: for y being real number st y in the carrier of R holds
x <= y
let z be real number ; ::_thesis: ( z in the carrier of R implies x <= z )
assume  z in the carrier of R ; ::_thesis: x <= z
hence  x <= z by A3, XXREAL_1:1; ::_thesis: verum
end;
then A4: R is lower-bounded by A1, Th6;
 ex x being real number st
( x in the carrier of R & ( for y being real number st y in the carrier of R holds
x >= y ) )
proof
take  y ; ::_thesis: ( y in the carrier of R & ( for y being real number st y in the carrier of R holds
y >= y ) )
thus  y in the carrier of R by A2, A3, XXREAL_1:1; ::_thesis: for y being real number st y in the carrier of R holds
y >= y
let z be real number ; ::_thesis: ( z in the carrier of R implies y >= z )
assume  z in the carrier of R ; ::_thesis: y >= z
hence  y >= z by A3, XXREAL_1:1; ::_thesis: verum
end;
then  R is upper-bounded by A1, Th7;
hence  R is bounded by A4; ::_thesis: verum
end;
end;

theorem Th8: :: LFUZZY_0:8
for R being non empty interval RelStr
for X being set holds ex_sup_of X,R
proof
let R be non empty interval RelStr ; ::_thesis: for X being set holds ex_sup_of X,R
let X be set ; ::_thesis: ex_sup_of X,R
consider a, b being real number  such that
A1: a <= b and
A2: the carrier of R = [.a,b.] by Def2;
reconsider a = a, b = b as Real by XREAL_0:def_1;
reconsider Y = X /\ [.a,b.] as Subset of REAL ;
 ( not [.a,b.] is empty & [.a,b.] is closed_interval ) by A1, MEASURE5:14;
then A3: [.a,b.] is bounded_above by INTEGRA1:3;
then A4: Y is bounded_above by XBOOLE_1:17, XXREAL_2:43;
A5: X /\ [.a,b.] c= [.a,b.] by XBOOLE_1:17;
 ex a being Element of R st
( Y is_<=_than a & ( for b being Element of R st Y is_<=_than b holds
a <<= b ) )
proof
percases ( Y is empty or not Y is empty ) ;
supposeA6: Y is empty ; ::_thesis: ex a being Element of R st
( Y is_<=_than a & ( for b being Element of R st Y is_<=_than b holds
a <<= b ) )
reconsider x = a as Element of R by A1, A2, XXREAL_1:1;
take  x ; ::_thesis: ( Y is_<=_than x & ( for b being Element of R st Y is_<=_than b holds
x <<= b ) )
thus  Y is_<=_than x by A6, YELLOW_0:6; ::_thesis: for b being Element of R st Y is_<=_than b holds
x <<= b
let y be Element of R; ::_thesis: ( Y is_<=_than y implies x <<= y )
 x <= y by A2, XXREAL_1:1;
hence  ( Y is_<=_than y implies x <<= y ) by Th3; ::_thesis: verum
end;
supposeA7: not Y is empty ; ::_thesis: ex a being Element of R st
( Y is_<=_than a & ( for b being Element of R st Y is_<=_than b holds
a <<= b ) )
set c = the Element of Y;
A8: the Element of Y in Y by A7;
then reconsider c = the Element of Y as Real ;
A9: a <= c by A5, A8, XXREAL_1:1;
 c <= upper_bound Y by A4, A7, SEQ_4:def_1;
then A10: a <= upper_bound Y by A9, XXREAL_0:2;
 upper_bound [.a,b.] = b by A1, JORDAN5A:19;
then  upper_bound Y <= b by A3, A7, SEQ_4:48, XBOOLE_1:17;
then reconsider x = upper_bound Y as Element of R by A2, A10, XXREAL_1:1;
A11: for y being Element of R st Y is_<=_than y holds
x <<= y
proof
let y be Element of R; ::_thesis: ( Y is_<=_than y implies x <<= y )
assume A12: Y is_<=_than y ; ::_thesis: x <<= y
 for z being real number st z in Y holds
z <= y
proof
let z be real number ; ::_thesis: ( z in Y implies z <= y )
assume A13: z in Y ; ::_thesis: z <= y
then reconsider z = z as Element of R by A2, XBOOLE_0:def_4;
 z <<= y by A12, A13, LATTICE3:def_9;
hence  z <= y by Th3; ::_thesis: verum
end;
then  upper_bound Y <= y by A7, SEQ_4:144;
hence  x <<= y by Th3; ::_thesis: verum
end;
take  x ; ::_thesis: ( Y is_<=_than x & ( for b being Element of R st Y is_<=_than b holds
x <<= b ) )
 for b being Element of R st b in Y holds
b <<= x
proof
let b be Element of R; ::_thesis: ( b in Y implies b <<= x )
assume  b in Y ; ::_thesis: b <<= x
then  b <= upper_bound Y by A4, SEQ_4:def_1;
hence  b <<= x by Th3; ::_thesis: verum
end;
hence  ( Y is_<=_than x & ( for b being Element of R st Y is_<=_than b holds
x <<= b ) ) by A11, LATTICE3:def_9; ::_thesis: verum
end;
end;
end;
then  ex_sup_of Y,R by YELLOW_0:15;
hence  ex_sup_of X,R by A2, YELLOW_0:50; ::_thesis: verum
end;

registration
cluster non empty interval  ->  non empty complete interval for RelStr ;
coherence
 for b1 being non empty interval RelStr holds b1 is complete
proof
let R be non empty interval RelStr ; ::_thesis: R is complete
 for X being Subset of R holds ex_sup_of X,R by Th8;
hence  R is complete by YELLOW_0:53; ::_thesis: verum
end;
end;

registration
cluster non empty reflexive transitive antisymmetric connected  ->  distributive for RelStr ;
coherence
 for b1 being Chain holds b1 is distributive
proof
let C be Chain; ::_thesis: C is distributive
 for x, y, z being Element of C holds x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z)
proof
let x, y, z be Element of C; ::_thesis: x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z)
A1: x <= x ;
percases ( ( x <= y & x <= z & y <= z ) or ( x <= y & x <= z & y >= z ) or ( x <= y & x >= z & y <= z ) or ( x <= y & x >= z & y >= z ) or ( x >= y & x <= z & y <= z ) or ( x >= y & x <= z & y >= z ) or ( x >= y & x >= z & y <= z ) or ( x >= y & x >= z & y >= z ) ) by WAYBEL_0:def_29;
supposeA2: ( x <= y & x <= z & y <= z ) ; ::_thesis: x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z)
then A3: x "/\" (y "\/" z) = x "/\" z by YELLOW_0:24
.= x by A2, YELLOW_0:25 ;
(x "/\" y) "\/" (x "/\" z) = x "\/" (x "/\" z) by A2, YELLOW_0:25
.= x "\/" x by A2, YELLOW_0:25
.= x by A1, YELLOW_0:24 ;
hence  x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) by A3; ::_thesis: verum
end;
supposeA4: ( x <= y & x <= z & y >= z ) ; ::_thesis: x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z)
then A5: x "/\" (y "\/" z) = x "/\" y by YELLOW_0:24
.= x by A4, YELLOW_0:25 ;
(x "/\" y) "\/" (x "/\" z) = x "\/" (x "/\" z) by A4, YELLOW_0:25
.= x "\/" x by A4, YELLOW_0:25
.= x by A1, YELLOW_0:24 ;
hence  x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) by A5; ::_thesis: verum
end;
supposeA6: ( x <= y & x >= z & y <= z ) ; ::_thesis: x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z)
then  z <= y by YELLOW_0:def_2;
then A7: z = y by A6, YELLOW_0:def_3;
A8: x "/\" (y "\/" z) = x "/\" z by A6, YELLOW_0:24
.= z by A6, YELLOW_0:25 ;
(x "/\" y) "\/" (x "/\" z) = x "\/" (x "/\" z) by A6, YELLOW_0:25
.= x "\/" z by A6, YELLOW_0:25
.= x by A6, YELLOW_0:24 ;
hence  x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) by A6, A7, A8, YELLOW_0:def_3; ::_thesis: verum
end;
supposeA9: ( x <= y & x >= z & y >= z ) ; ::_thesis: x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z)
then A10: x "/\" (y "\/" z) = x "/\" y by YELLOW_0:24
.= x by A9, YELLOW_0:25 ;
(x "/\" y) "\/" (x "/\" z) = x "\/" (x "/\" z) by A9, YELLOW_0:25
.= x "\/" z by A9, YELLOW_0:25
.= x by A9, YELLOW_0:24 ;
hence  x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) by A10; ::_thesis: verum
end;
supposeA11: ( x >= y & x <= z & y <= z ) ; ::_thesis: x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z)
then A12: x "/\" (y "\/" z) = x "/\" z by YELLOW_0:24
.= x by A11, YELLOW_0:25 ;
(x "/\" y) "\/" (x "/\" z) = y "\/" (x "/\" z) by A11, YELLOW_0:25
.= y "\/" x by A11, YELLOW_0:25
.= x by A11, YELLOW_0:24 ;
hence  x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) by A12; ::_thesis: verum
end;
supposeA13: ( x >= y & x <= z & y >= z ) ; ::_thesis: x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z)
then  z >= y by YELLOW_0:def_2;
then A14: z = y by A13, YELLOW_0:def_3;
A15: x "/\" (y "\/" z) = x "/\" y by A13, YELLOW_0:24
.= y by A13, YELLOW_0:25 ;
(x "/\" y) "\/" (x "/\" z) = y "\/" (x "/\" z) by A13, YELLOW_0:25
.= y "\/" x by A13, YELLOW_0:25
.= x by A13, YELLOW_0:24 ;
hence  x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) by A13, A14, A15, YELLOW_0:def_3; ::_thesis: verum
end;
supposeA16: ( x >= y & x >= z & y <= z ) ; ::_thesis: x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z)
then A17: x "/\" (y "\/" z) = x "/\" z by YELLOW_0:24
.= z by A16, YELLOW_0:25 ;
(x "/\" y) "\/" (x "/\" z) = y "\/" (x "/\" z) by A16, YELLOW_0:25
.= y "\/" z by A16, YELLOW_0:25
.= z by A16, YELLOW_0:24 ;
hence  x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) by A17; ::_thesis: verum
end;
supposeA18: ( x >= y & x >= z & y >= z ) ; ::_thesis: x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z)
then A19: x "/\" (y "\/" z) = x "/\" y by YELLOW_0:24
.= y by A18, YELLOW_0:25 ;
(x "/\" y) "\/" (x "/\" z) = y "\/" (x "/\" z) by A18, YELLOW_0:25
.= y "\/" z by A18, YELLOW_0:25
.= y by A18, YELLOW_0:24 ;
hence  x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) by A19; ::_thesis: verum
end;
end;
end;
hence  C is distributive by WAYBEL_1:def_3; ::_thesis: verum
end;
end;

registration
cluster non empty interval  ->  non empty Heyting interval for RelStr ;
coherence
 for b1 being non empty interval RelStr holds b1 is Heyting
proof
let R be non empty interval RelStr ; ::_thesis: R is Heyting
thus  R is LATTICE ; :: according to WAYBEL_1:def_19 ::_thesis: for b1 being Element of the carrier of R holds b1 "/\" is lower_adjoint
let x be Element of R; ::_thesis: x "/\" is lower_adjoint
set f = x "/\" ;
 x "/\" is sups-preserving
proof
let X be Subset of R; :: according to WAYBEL_0:def_33 ::_thesis: x "/\" preserves_sup_of X
assume  ex_sup_of X,R ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of (x "/\") .: X,R & "\/" (((x "/\") .: X),R) = (x "/\") . ("\/" (X,R)) )
A1: now__::_thesis:_for_b_being_Element_of_R_st_b_is_>=_than_(x_"/\")_.:_X_holds_
(x_"/\")_._(sup_X)_<<=_b
let b be Element of R; ::_thesis: ( b is_>=_than (x "/\") .: X implies (x "/\") . (sup X) <<= b1 )
assume A2: b is_>=_than (x "/\") .: X ; ::_thesis: (x "/\") . (sup X) <<= b1
percases ( x is_>=_than X or not x is_>=_than X ) ;
supposeA3: x is_>=_than X ; ::_thesis: (x "/\") . (sup X) <<= b1
 b is_>=_than X
proof
let a be Element of R; :: according to LATTICE3:def_9 ::_thesis: ( not a in X or a <<= b )
assume A4: a in X ; ::_thesis: a <<= b
then  x >>= a by A3, LATTICE3:def_9;
then  x "/\" a = a by YELLOW_0:25;
then A5: a = (x "/\") . a by WAYBEL_1:def_18;
 (x "/\") . a in (x "/\") .: X by A4, FUNCT_2:35;
hence  a <<= b by A2, A5, LATTICE3:def_9; ::_thesis: verum
end;
then A6: b >>= sup X by YELLOW_0:32;
 x >>= sup X by A3, YELLOW_0:32;
then  x "/\" (sup X) = sup X by YELLOW_0:25;
hence  (x "/\") . (sup X) <<= b by A6, WAYBEL_1:def_18; ::_thesis: verum
end;
suppose not x is_>=_than X ; ::_thesis: (x "/\") . (sup X) <<= b1
then consider a being Element of R such that
A7: a in X and
A8: not x >>= a by LATTICE3:def_9;
A9: x <<= a by A8, WAYBEL_0:def_29;
 a <<= sup X by A7, YELLOW_2:22;
then  x <<= sup X by A9, ORDERS_2:3;
then  x = x "/\" (sup X) by YELLOW_0:25;
then A10: x = (x "/\") . (sup X) by WAYBEL_1:def_18;
A11: (x "/\") . a in (x "/\") .: X by A7, FUNCT_2:35;
x = x "/\" a by A9, YELLOW_0:25
.= (x "/\") . a by WAYBEL_1:def_18 ;
hence  (x "/\") . (sup X) <<= b by A2, A10, A11, LATTICE3:def_9; ::_thesis: verum
end;
end;
end;
thus  ex_sup_of (x "/\") .: X,R by Th8; ::_thesis: "\/" (((x "/\") .: X),R) = (x "/\") . ("\/" (X,R))
 (x "/\") . (sup X) is_>=_than (x "/\") .: X
proof
let a be Element of R; :: according to LATTICE3:def_9 ::_thesis: ( not a in (x "/\") .: X or a <<= (x "/\") . (sup X) )
A12: ( (x "/\") . (sup X) = x "/\" (sup X) & x <<= x ) by WAYBEL_1:def_18, YELLOW_0:def_1;
assume  a in (x "/\") .: X ; ::_thesis: a <<= (x "/\") . (sup X)
then consider y being set  such that
A13: y in the carrier of R and
A14: ( y in X & a = (x "/\") . y ) by FUNCT_2:64;
reconsider y = y as Element of R by A13;
 ( y <<= sup X & a = x "/\" y ) by A14, WAYBEL_1:def_18, YELLOW_2:22;
hence  a <<= (x "/\") . (sup X) by A12, YELLOW_3:2; ::_thesis: verum
end;
hence  "\/" (((x "/\") .: X),R) = (x "/\") . ("\/" (X,R)) by A1, YELLOW_0:30; ::_thesis: verum
end;
hence  x "/\" is lower_adjoint by WAYBEL_1:17; ::_thesis: verum
end;
end;

registration
clusterK582(0,1) ->  non empty ;
coherence
 not [.0,1.] is empty by MEASURE5:14;
end;

registration
cluster RealPoset [.0,1.] ->  strict real interval ;
coherence
 RealPoset [.0,1.] is interval
proof
 the carrier of (RealPoset [.0,1.]) = [.0,1.] by Def3;
hence  RealPoset [.0,1.] is interval by Def2; ::_thesis: verum
end;
end;

begin

theorem Th9: :: LFUZZY_0:9
for I being non empty set
for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st ( for i being Element of I holds J . i is sup-Semilattice ) holds
product J is with_suprema
proof
let I be non empty set ; ::_thesis: for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st ( for i being Element of I holds J . i is sup-Semilattice ) holds
product J is with_suprema
let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I; ::_thesis: ( ( for i being Element of I holds J . i is sup-Semilattice ) implies product J is with_suprema )
assume A1: for i being Element of I holds J . i is sup-Semilattice ; ::_thesis: product J is with_suprema
set IT = product J;
 for x, y being Element of (product J) ex z being Element of (product J) st
( x <= z & y <= z & ( for z9 being Element of (product J) st x <= z9 & y <= z9 holds
z <= z9 ) )
proof
let x, y be Element of (product J); ::_thesis: ex z being Element of (product J) st
( x <= z & y <= z & ( for z9 being Element of (product J) st x <= z9 & y <= z9 holds
z <= z9 ) )
deffunc H1( Element of I) ->  Element of the carrier of (J . $1) = (x . $1) "\/" (y . $1);
consider z being ManySortedSet of I such that
A2: for i being Element of I holds z . i = H1(i) from PBOOLE:sch_5();
A3: for i being Element of I holds z . i is Element of (J . i)
proof
let i be Element of I; ::_thesis: z . i is Element of (J . i)
 z . i = (x . i) "\/" (y . i) by A2;
hence  z . i is Element of (J . i) ; ::_thesis: verum
end;
 dom z = I by PARTFUN1:def_2;
then reconsider z = z as Element of (product J) by A3, WAYBEL_3:27;
take  z ; ::_thesis: ( x <= z & y <= z & ( for z9 being Element of (product J) st x <= z9 & y <= z9 holds
z <= z9 ) )
 for i being Element of I holds
( x . i <= z . i & y . i <= z . i )
proof
let i be Element of I; ::_thesis: ( x . i <= z . i & y . i <= z . i )
 ( J . i is antisymmetric with_suprema RelStr & z . i = (x . i) "\/" (y . i) ) by A1, A2;
hence  ( x . i <= z . i & y . i <= z . i ) by YELLOW_0:22; ::_thesis: verum
end;
hence  ( x <= z & y <= z ) by WAYBEL_3:28; ::_thesis: for z9 being Element of (product J) st x <= z9 & y <= z9 holds
z <= z9
let z9 be Element of (product J); ::_thesis: ( x <= z9 & y <= z9 implies z <= z9 )
assume that
A4: x <= z9 and
A5: y <= z9 ; ::_thesis: z <= z9
 for i being Element of I holds z . i <= z9 . i
proof
let i be Element of I; ::_thesis: z . i <= z9 . i
A6: ( z9 . i >= y . i & z . i = (x . i) "\/" (y . i) ) by A2, A5, WAYBEL_3:28;
 ( J . i is antisymmetric with_suprema RelStr & z9 . i >= x . i ) by A1, A4, WAYBEL_3:28;
hence  z . i <= z9 . i by A6, YELLOW_0:22; ::_thesis: verum
end;
hence  z <= z9 by WAYBEL_3:28; ::_thesis: verum
end;
hence  product J is with_suprema by LATTICE3:def_10; ::_thesis: verum
end;

theorem Th10: :: LFUZZY_0:10
for I being non empty set
for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st ( for i being Element of I holds J . i is Semilattice ) holds
product J is with_infima
proof
let I be non empty set ; ::_thesis: for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st ( for i being Element of I holds J . i is Semilattice ) holds
product J is with_infima
let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I; ::_thesis: ( ( for i being Element of I holds J . i is Semilattice ) implies product J is with_infima )
assume A1: for i being Element of I holds J . i is Semilattice ; ::_thesis: product J is with_infima
set IT = product J;
 for x, y being Element of (product J) ex z being Element of (product J) st
( x >= z & y >= z & ( for z9 being Element of (product J) st x >= z9 & y >= z9 holds
z >= z9 ) )
proof
let x, y be Element of (product J); ::_thesis: ex z being Element of (product J) st
( x >= z & y >= z & ( for z9 being Element of (product J) st x >= z9 & y >= z9 holds
z >= z9 ) )
deffunc H1( Element of I) ->  Element of the carrier of (J . $1) = (x . $1) "/\" (y . $1);
consider z being ManySortedSet of I such that
A2: for i being Element of I holds z . i = H1(i) from PBOOLE:sch_5();
A3: for i being Element of I holds z . i is Element of (J . i)
proof
let i be Element of I; ::_thesis: z . i is Element of (J . i)
 z . i = (x . i) "/\" (y . i) by A2;
hence  z . i is Element of (J . i) ; ::_thesis: verum
end;
 dom z = I by PARTFUN1:def_2;
then reconsider z = z as Element of (product J) by A3, WAYBEL_3:27;
take  z ; ::_thesis: ( x >= z & y >= z & ( for z9 being Element of (product J) st x >= z9 & y >= z9 holds
z >= z9 ) )
 for i being Element of I holds
( x . i >= z . i & y . i >= z . i )
proof
let i be Element of I; ::_thesis: ( x . i >= z . i & y . i >= z . i )
 ( J . i is antisymmetric with_infima RelStr & z . i = (x . i) "/\" (y . i) ) by A1, A2;
hence  ( x . i >= z . i & y . i >= z . i ) by YELLOW_0:23; ::_thesis: verum
end;
hence  ( x >= z & y >= z ) by WAYBEL_3:28; ::_thesis: for z9 being Element of (product J) st x >= z9 & y >= z9 holds
z >= z9
let z9 be Element of (product J); ::_thesis: ( x >= z9 & y >= z9 implies z >= z9 )
assume that
A4: x >= z9 and
A5: y >= z9 ; ::_thesis: z >= z9
 for i being Element of I holds z . i >= z9 . i
proof
let i be Element of I; ::_thesis: z . i >= z9 . i
A6: ( z9 . i <= y . i & z . i = (x . i) "/\" (y . i) ) by A2, A5, WAYBEL_3:28;
 ( J . i is antisymmetric with_infima RelStr & x . i >= z9 . i ) by A1, A4, WAYBEL_3:28;
hence  z . i >= z9 . i by A6, YELLOW_0:23; ::_thesis: verum
end;
hence  z >= z9 by WAYBEL_3:28; ::_thesis: verum
end;
hence  product J is with_infima by LATTICE3:def_11; ::_thesis: verum
end;

theorem Th11: :: LFUZZY_0:11
for I being non empty set
for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st ( for i being Element of I holds J . i is Semilattice ) holds
for f, g being Element of (product J)
for i being Element of I holds (f "/\" g) . i = (f . i) "/\" (g . i)
proof
let I be non empty set ; ::_thesis: for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st ( for i being Element of I holds J . i is Semilattice ) holds
for f, g being Element of (product J)
for i being Element of I holds (f "/\" g) . i = (f . i) "/\" (g . i)
let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I; ::_thesis: ( ( for i being Element of I holds J . i is Semilattice ) implies for f, g being Element of (product J)
for i being Element of I holds (f "/\" g) . i = (f . i) "/\" (g . i) )
assume A1: for i being Element of I holds J . i is Semilattice ; ::_thesis: for f, g being Element of (product J)
for i being Element of I holds (f "/\" g) . i = (f . i) "/\" (g . i)
let f, g be Element of (product J); ::_thesis: for i being Element of I holds (f "/\" g) . i = (f . i) "/\" (g . i)
let i be Element of I; ::_thesis: (f "/\" g) . i = (f . i) "/\" (g . i)
A2: J . i is Semilattice by A1;
 for i being Element of I holds J . i is antisymmetric by A1;
then A3: ( product J is antisymmetric & product J is with_infima ) by A1, Th10, WAYBEL_3:30;
then  g >= f "/\" g by YELLOW_0:23;
then A4: g . i >= (f "/\" g) . i by WAYBEL_3:28;
A5: (f "/\" g) . i >= (f . i) "/\" (g . i)
proof
deffunc H1( Element of I) ->  Element of the carrier of (J . $1) = (f . $1) "/\" (g . $1);
consider z being ManySortedSet of I such that
A6: for i being Element of I holds z . i = H1(i) from PBOOLE:sch_5();
A7: for i being Element of I holds z . i is Element of (J . i)
proof
let i be Element of I; ::_thesis: z . i is Element of (J . i)
 z . i = (f . i) "/\" (g . i) by A6;
hence  z . i is Element of (J . i) ; ::_thesis: verum
end;
 dom z = I by PARTFUN1:def_2;
then reconsider z = z as Element of (product J) by A7, WAYBEL_3:27;
 for i being Element of I holds
( z . i <= f . i & z . i <= g . i )
proof
let i be Element of I; ::_thesis: ( z . i <= f . i & z . i <= g . i )
 ( J . i is antisymmetric with_infima RelStr & z . i = (f . i) "/\" (g . i) ) by A1, A6;
hence  ( z . i <= f . i & z . i <= g . i ) by YELLOW_0:23; ::_thesis: verum
end;
then  ( z <= f & z <= g ) by WAYBEL_3:28;
then A8: f "/\" g >= z by A3, YELLOW_0:23;
 for i being Element of I holds (f "/\" g) . i >= (f . i) "/\" (g . i)
proof
let i be Element of I; ::_thesis: (f "/\" g) . i >= (f . i) "/\" (g . i)
 (f . i) "/\" (g . i) = z . i by A6;
hence  (f "/\" g) . i >= (f . i) "/\" (g . i) by A8, WAYBEL_3:28; ::_thesis: verum
end;
hence  (f "/\" g) . i >= (f . i) "/\" (g . i) ; ::_thesis: verum
end;
 f >= f "/\" g by A3, YELLOW_0:23;
then  f . i >= (f "/\" g) . i by WAYBEL_3:28;
then  (f "/\" g) . i <= (f . i) "/\" (g . i) by A2, A4, YELLOW_0:23;
hence  (f "/\" g) . i = (f . i) "/\" (g . i) by A2, A5, YELLOW_0:def_3; ::_thesis: verum
end;

theorem Th12: :: LFUZZY_0:12
for I being non empty set
for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st ( for i being Element of I holds J . i is sup-Semilattice ) holds
for f, g being Element of (product J)
for i being Element of I holds (f "\/" g) . i = (f . i) "\/" (g . i)
proof
let I be non empty set ; ::_thesis: for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st ( for i being Element of I holds J . i is sup-Semilattice ) holds
for f, g being Element of (product J)
for i being Element of I holds (f "\/" g) . i = (f . i) "\/" (g . i)
let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I; ::_thesis: ( ( for i being Element of I holds J . i is sup-Semilattice ) implies for f, g being Element of (product J)
for i being Element of I holds (f "\/" g) . i = (f . i) "\/" (g . i) )
assume A1: for i being Element of I holds J . i is sup-Semilattice ; ::_thesis: for f, g being Element of (product J)
for i being Element of I holds (f "\/" g) . i = (f . i) "\/" (g . i)
let f, g be Element of (product J); ::_thesis: for i being Element of I holds (f "\/" g) . i = (f . i) "\/" (g . i)
let i be Element of I; ::_thesis: (f "\/" g) . i = (f . i) "\/" (g . i)
A2: J . i is sup-Semilattice by A1;
 for i being Element of I holds J . i is antisymmetric by A1;
then A3: ( product J is antisymmetric & product J is with_suprema ) by A1, Th9, WAYBEL_3:30;
then  g <= f "\/" g by YELLOW_0:22;
then A4: g . i <= (f "\/" g) . i by WAYBEL_3:28;
A5: (f "\/" g) . i <= (f . i) "\/" (g . i)
proof
deffunc H1( Element of I) ->  Element of the carrier of (J . $1) = (f . $1) "\/" (g . $1);
consider z being ManySortedSet of I such that
A6: for i being Element of I holds z . i = H1(i) from PBOOLE:sch_5();
A7: for i being Element of I holds z . i is Element of (J . i)
proof
let i be Element of I; ::_thesis: z . i is Element of (J . i)
 z . i = (f . i) "\/" (g . i) by A6;
hence  z . i is Element of (J . i) ; ::_thesis: verum
end;
 dom z = I by PARTFUN1:def_2;
then reconsider z = z as Element of (product J) by A7, WAYBEL_3:27;
 for i being Element of I holds
( z . i >= f . i & z . i >= g . i )
proof
let i be Element of I; ::_thesis: ( z . i >= f . i & z . i >= g . i )
 ( J . i is antisymmetric with_suprema RelStr & z . i = (f . i) "\/" (g . i) ) by A1, A6;
hence  ( z . i >= f . i & z . i >= g . i ) by YELLOW_0:22; ::_thesis: verum
end;
then  ( z >= f & z >= g ) by WAYBEL_3:28;
then A8: f "\/" g <= z by A3, YELLOW_0:22;
 for i being Element of I holds (f "\/" g) . i <= (f . i) "\/" (g . i)
proof
let i be Element of I; ::_thesis: (f "\/" g) . i <= (f . i) "\/" (g . i)
 (f . i) "\/" (g . i) = z . i by A6;
hence  (f "\/" g) . i <= (f . i) "\/" (g . i) by A8, WAYBEL_3:28; ::_thesis: verum
end;
hence  (f "\/" g) . i <= (f . i) "\/" (g . i) ; ::_thesis: verum
end;
 f <= f "\/" g by A3, YELLOW_0:22;
then  f . i <= (f "\/" g) . i by WAYBEL_3:28;
then  (f "\/" g) . i >= (f . i) "\/" (g . i) by A2, A4, YELLOW_0:22;
hence  (f "\/" g) . i = (f . i) "\/" (g . i) by A2, A5, YELLOW_0:def_3; ::_thesis: verum
end;

theorem Th13: :: LFUZZY_0:13
for I being non empty set
for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st ( for i being Element of I holds J . i is complete Heyting LATTICE ) holds
( product J is complete & product J is Heyting )
proof
let I be non empty set ; ::_thesis: for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st ( for i being Element of I holds J . i is complete Heyting LATTICE ) holds
( product J is complete & product J is Heyting )
let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I; ::_thesis: ( ( for i being Element of I holds J . i is complete Heyting LATTICE ) implies ( product J is complete & product J is Heyting ) )
assume A1: for i being Element of I holds J . i is complete Heyting LATTICE ; ::_thesis: ( product J is complete & product J is Heyting )
A2: for i being Element of I holds J . i is complete LATTICE by A1;
set H = product J;
reconsider H = product J as complete LATTICE by A2, WAYBEL_3:31;
 H = H ;
hence  ( product J is complete & product J is LATTICE ) ; :: according to WAYBEL_1:def_19 ::_thesis: for b1 being Element of the carrier of (product J) holds b1 "/\" is lower_adjoint
let f be Element of (product J); ::_thesis: f "/\" is lower_adjoint
reconsider g = f as Element of H ;
reconsider F = f "/\" as Function of H,H ;
A3: for i being Element of I holds J . i is Semilattice by A1;
 F is sups-preserving
proof
let X be Subset of H; :: according to WAYBEL_0:def_33 ::_thesis: F preserves_sup_of X
reconsider Y = F .: X, X9 = X as Subset of (product J) ;
reconsider sX = sup X as Element of (product J) ;
assume  ex_sup_of X,H ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of F .: X,H & "\/" ((F .: X),H) = F . ("\/" (X,H)) )
thus  ex_sup_of F .: X,H by YELLOW_0:17; ::_thesis: "\/" ((F .: X),H) = F . ("\/" (X,H))
reconsider f1 = sup (F .: X), f2 = F . (sup X) as Element of (product J) ;
A4: now__::_thesis:_for_x_being_set_st_x_in_dom_f1_holds_
f1_._x_=_f2_._x
let x be set ; ::_thesis: ( x in dom f1 implies f1 . x = f2 . x )
assume  x in dom f1 ; ::_thesis: f1 . x = f2 . x
then reconsider i = x as Element of I by WAYBEL_3:27;
A5: J . i is complete Heyting LATTICE by A1;
then A6: ex_sup_of pi (X9,i),J . i by YELLOW_0:17;
A7: ((f . i) "/\") .: (pi (X9,i)) c= pi (Y,i)
proof
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in ((f . i) "/\") .: (pi (X9,i)) or b in pi (Y,i) )
assume  b in ((f . i) "/\") .: (pi (X9,i)) ; ::_thesis: b in pi (Y,i)
then consider f4 being set  such that
 f4 in dom ((f . i) "/\") and
A8: f4 in pi (X9,i) and
A9: b = ((f . i) "/\") . f4 by FUNCT_1:def_6;
consider f5 being Function such that
A10: f5 in X9 and
A11: f4 = f5 . i by A8, CARD_3:def_6;
reconsider f5 = f5 as Element of (product J) by A10;
 f "/\" f5 = (f "/\") . f5 by WAYBEL_1:def_18;
then A12: f "/\" f5 in (f "/\") .: X by A10, FUNCT_2:35;
((f . i) "/\") . f4 = (f . i) "/\" (f5 . i) by A11, WAYBEL_1:def_18
.= (f "/\" f5) . i by A3, Th11 ;
hence  b in pi (Y,i) by A9, A12, CARD_3:def_6; ::_thesis: verum
end;
 pi (Y,i) c= ((f . i) "/\") .: (pi (X9,i))
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in pi (Y,i) or a in ((f . i) "/\") .: (pi (X9,i)) )
assume  a in pi (Y,i) ; ::_thesis: a in ((f . i) "/\") .: (pi (X9,i))
then consider f3 being Function such that
A13: f3 in Y and
A14: a = f3 . i by CARD_3:def_6;
reconsider f3 = f3 as Element of (product J) by A13;
consider h being set  such that
A15: h in dom F and
A16: h in X and
A17: f3 = F . h by A13, FUNCT_1:def_6;
reconsider h = h as Element of (product J) by A15;
A18: h . i in pi (X9,i) by A16, CARD_3:def_6;
f3 . i = (f "/\" h) . i by A17, WAYBEL_1:def_18
.= (f . i) "/\" (h . i) by A3, Th11
.= ((f . i) "/\") . (h . i) by WAYBEL_1:def_18 ;
hence  a in ((f . i) "/\") .: (pi (X9,i)) by A14, A18, FUNCT_2:35; ::_thesis: verum
end;
then A19: pi (Y,i) = ((f . i) "/\") .: (pi (X9,i)) by A7, XBOOLE_0:def_10;
 (f . i) "/\" is lower_adjoint by A5, WAYBEL_1:def_19;
then A20: (f . i) "/\" preserves_sup_of pi (X9,i) by A5, WAYBEL_0:def_33;
 f2 = g "/\" (sup X) by WAYBEL_1:def_18;
then f2 . i = (f . i) "/\" (sX . i) by A3, Th11
.= (f . i) "/\" (sup (pi (X9,i))) by A2, WAYBEL_3:32
.= ((f . i) "/\") . (sup (pi (X9,i))) by WAYBEL_1:def_18
.= sup (((f . i) "/\") .: (pi (X9,i))) by A20, A6, WAYBEL_0:def_31 ;
hence  f1 . x = f2 . x by A2, A19, WAYBEL_3:32; ::_thesis: verum
end;
 ( dom f1 = I & dom f2 = I ) by WAYBEL_3:27;
hence  "\/" ((F .: X),H) = F . ("\/" (X,H)) by A4, FUNCT_1:2; ::_thesis: verum
end;
hence  f "/\" is lower_adjoint by WAYBEL_1:17; ::_thesis: verum
end;

registration
let A be non empty set ;
let R be complete Heyting LATTICE;
clusterR |^ A ->  Heyting ;
coherence
 R |^ A is Heyting
proof
 for i being Element of A holds (A --> R) . i is complete Heyting LATTICE by FUNCOP_1:7;
then  ( product (A --> R) is complete & product (A --> R) is Heyting ) by Th13;
hence  R |^ A is Heyting by YELLOW_1:def_5; ::_thesis: verum
end;
end;

begin

definition
let A be non empty set ;
func FuzzyLattice A ->  complete Heyting LATTICE equals :: LFUZZY_0:def 4
(RealPoset [.0,1.]) |^ A;
coherence
 (RealPoset [.0,1.]) |^ A is complete Heyting LATTICE ;
end;

:: deftheorem  defines FuzzyLattice LFUZZY_0:def_4_:_
 for A being non empty set holds FuzzyLattice A = (RealPoset [.0,1.]) |^ A;

theorem Th14: :: LFUZZY_0:14
for A being non empty set holds the carrier of (FuzzyLattice A) = Funcs (A,[.0,1.])
proof
let A be non empty set ; ::_thesis: the carrier of (FuzzyLattice A) = Funcs (A,[.0,1.])
thus  the carrier of (FuzzyLattice A) = Funcs (A, the carrier of (RealPoset [.0,1.])) by YELLOW_1:28
.= Funcs (A,[.0,1.]) by Def3 ; ::_thesis: verum
end;

Lm1:  for A being non empty set holds FuzzyLattice A is constituted-Functions
proof
let A be non empty set ; ::_thesis: FuzzyLattice A is constituted-Functions
 for a being Element of (FuzzyLattice A) holds a is Function
proof
let a be Element of (FuzzyLattice A); ::_thesis: a is Function
 a in the carrier of (FuzzyLattice A) ;
then  a in Funcs (A,[.0,1.]) by Th14;
then  ex f being Function st
( a = f & dom f = A & rng f c= [.0,1.] ) by FUNCT_2:def_2;
hence  a is Function ; ::_thesis: verum
end;
hence  FuzzyLattice A is constituted-Functions by MONOID_0:def_1; ::_thesis: verum
end;

registration
let A be non empty set ;
cluster FuzzyLattice A ->  complete constituted-Functions Heyting ;
coherence
 FuzzyLattice A is constituted-Functions by Lm1;
end;

theorem Th15: :: LFUZZY_0:15
for R being complete Heyting LATTICE
for X being Subset of R
for y being Element of R holds ("\/" (X,R)) "/\" y = "\/" ( {  (x "/\" y) where x is Element of R : x in X  }  ,R)
proof
let R be complete Heyting LATTICE; ::_thesis: for X being Subset of R
for y being Element of R holds ("\/" (X,R)) "/\" y = "\/" ( {  (x "/\" y) where x is Element of R : x in X  }  ,R)
let X be Subset of R; ::_thesis: for y being Element of R holds ("\/" (X,R)) "/\" y = "\/" ( {  (x "/\" y) where x is Element of R : x in X  }  ,R)
let y be Element of R; ::_thesis: ("\/" (X,R)) "/\" y = "\/" ( {  (x "/\" y) where x is Element of R : x in X  }  ,R)
set Z =  {  (y "/\" x) where x is Element of R : x in X  }  ;
set W =  {  (x "/\" y) where x is Element of R : x in X  }  ;
A1:  {  (x "/\" y) where x is Element of R : x in X  }  c=  {  (y "/\" x) where x is Element of R : x in X  }
proof
let w be set ; :: according to TARSKI:def_3 ::_thesis: ( not w in  {  (x "/\" y) where x is Element of R : x in X  }  or w in  {  (y "/\" x) where x is Element of R : x in X  }  )
assume  w in  {  (x "/\" y) where x is Element of R : x in X  }  ; ::_thesis: w in  {  (y "/\" x) where x is Element of R : x in X  }
then  ex x being Element of R st
( w = x "/\" y & x in X ) ;
hence  w in  {  (y "/\" x) where x is Element of R : x in X  }  ; ::_thesis: verum
end;
  {  (y "/\" x) where x is Element of R : x in X  }  c=  {  (x "/\" y) where x is Element of R : x in X  }
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in  {  (y "/\" x) where x is Element of R : x in X  }  or z in  {  (x "/\" y) where x is Element of R : x in X  }  )
assume  z in  {  (y "/\" x) where x is Element of R : x in X  }  ; ::_thesis: z in  {  (x "/\" y) where x is Element of R : x in X  }
then  ex x being Element of R st
( z = y "/\" x & x in X ) ;
hence  z in  {  (x "/\" y) where x is Element of R : x in X  }  ; ::_thesis: verum
end;
then  ( ( for z being Element of R holds
( z "/\" is lower_adjoint & ex_sup_of X,R ) ) &  {  (y "/\" x) where x is Element of R : x in X  }  =  {  (x "/\" y) where x is Element of R : x in X  }  ) by A1, WAYBEL_1:def_19, XBOOLE_0:def_10, YELLOW_0:17;
hence  ("\/" (X,R)) "/\" y = "\/" ( {  (x "/\" y) where x is Element of R : x in X  }  ,R) by WAYBEL_1:63; ::_thesis: verum
end;

Lm2:  for X being non empty set
for a being Element of (FuzzyLattice X) holds a is Membership_Func of X
proof
let X be non empty set ; ::_thesis: for a being Element of (FuzzyLattice X) holds a is Membership_Func of X
let a be Element of (FuzzyLattice X); ::_thesis: a is Membership_Func of X
 a in the carrier of (FuzzyLattice X) ;
then  a in Funcs (X,[.0,1.]) by Th14;
then A1: ex f being Function st
( a = f & dom f = X & rng f c= [.0,1.] ) by FUNCT_2:def_2;
then reconsider a = a as PartFunc of X,[.0,1.] by RELSET_1:4;
reconsider a = a as PartFunc of X,REAL by RELSET_1:7;
 a is Function of X,REAL by A1, FUNCT_2:def_1;
hence  a is Membership_Func of X ; ::_thesis: verum
end;

definition
let X be non empty set ;
let a be Element of (FuzzyLattice X);
func @ a ->  Membership_Func of X equals :: LFUZZY_0:def 5
a;
coherence
 a is Membership_Func of X by Lm2;
end;

:: deftheorem  defines @ LFUZZY_0:def_5_:_
 for X being non empty set
for a being Element of (FuzzyLattice X) holds @ a = a;

Lm3:  for X being non empty set
for f being Membership_Func of X holds f is Element of (FuzzyLattice X)
proof
let X be non empty set ; ::_thesis: for f being Membership_Func of X holds f is Element of (FuzzyLattice X)
let f be Membership_Func of X; ::_thesis: f is Element of (FuzzyLattice X)
 ( dom f = X & rng f c= [.0,1.] ) by FUNCT_2:def_1, RELAT_1:def_19;
then  f in Funcs (X,[.0,1.]) by FUNCT_2:def_2;
hence  f is Element of (FuzzyLattice X) by Th14; ::_thesis: verum
end;

definition
let X be non empty set ;
let f be Membership_Func of X;
func(X,f) @  ->  Element of (FuzzyLattice X) equals :: LFUZZY_0:def 6
f;
coherence
 f is Element of (FuzzyLattice X) by Lm3;
end;

:: deftheorem  defines @ LFUZZY_0:def_6_:_
 for X being non empty set
for f being Membership_Func of X holds (X,f) @ = f;

definition
let X be non empty set ;
let f be Membership_Func of X;
let x be Element of X;
:: original: .
redefine funcf . x ->  Element of (RealPoset [.0,1.]);
coherence
 f . x is Element of (RealPoset [.0,1.])
proof
 ( 0 <= f . x & f . x <= 1 ) by FUZZY_2:1;
then  f . x in [.0,1.] by XXREAL_1:1;
hence  f . x is Element of (RealPoset [.0,1.]) by Def3; ::_thesis: verum
end;
end;

definition
let X, Y be non empty set ;
let f be RMembership_Func of X,Y;
let x be Element of X;
let y be Element of Y;
:: original: .
redefine funcf . (x,y) ->  Element of (RealPoset [.0,1.]);
coherence
 f . (x,y) is Element of (RealPoset [.0,1.])
proof
 f . [x,y] is Element of (RealPoset [.0,1.]) ;
hence  f . (x,y) is Element of (RealPoset [.0,1.]) ; ::_thesis: verum
end;
end;

definition
let X be non empty set ;
let f be Element of (FuzzyLattice X);
let x be Element of X;
:: original: .
redefine funcf . x ->  Element of (RealPoset [.0,1.]);
coherence
 f . x is Element of (RealPoset [.0,1.])
proof
 0 <= (@ f) . x by FUZZY_2:1;
hence  f . x is Element of (RealPoset [.0,1.]) ; ::_thesis: verum
end;
end;


theorem Th16: :: LFUZZY_0:16
for C being non empty set
for f, g being Membership_Func of C holds
( ( for c being Element of C holds f . c <= g . c ) iff (C,f) @ <<= (C,g) @ )
proof
let C be non empty set ; ::_thesis: for f, g being Membership_Func of C holds
( ( for c being Element of C holds f . c <= g . c ) iff (C,f) @ <<= (C,g) @ )
let f, g be Membership_Func of C; ::_thesis: ( ( for c being Element of C holds f . c <= g . c ) iff (C,f) @ <<= (C,g) @ )
A1: (RealPoset [.0,1.]) |^ C = product (C --> (RealPoset [.0,1.])) by YELLOW_1:def_5;
A2: ( ( for c being Element of C holds f . c <= g . c ) implies (C,f) @ <<= (C,g) @ )
proof
set f9 = (C,f) @ ;
set g9 = (C,g) @ ;
reconsider f9 = (C,f) @ , g9 = (C,g) @ as Element of (product (C --> (RealPoset [.0,1.]))) by YELLOW_1:def_5;
assume A3: for c being Element of C holds f . c <= g . c ; ::_thesis: (C,f) @ <<= (C,g) @
 for c being Element of C holds f9 . c <<= g9 . c
proof
let c be Element of C; ::_thesis: f9 . c <<= g9 . c
set f1 = f . c;
set g1 = g . c;
 ( (C --> (RealPoset [.0,1.])) . c = RealPoset [.0,1.] & f . c <= g . c ) by A3, FUNCOP_1:7;
hence  f9 . c <<= g9 . c by Th3; ::_thesis: verum
end;
hence  (C,f) @ <<= (C,g) @ by A1, WAYBEL_3:28; ::_thesis: verum
end;
 ( (C,f) @ <<= (C,g) @ implies for c being Element of C holds f . c <= g . c )
proof
reconsider ff = (C,f) @ , gg = (C,g) @ as Element of (product (C --> (RealPoset [.0,1.]))) by YELLOW_1:def_5;
assume A4: (C,f) @ <<= (C,g) @ ; ::_thesis: for c being Element of C holds f . c <= g . c
let c be Element of C; ::_thesis: f . c <= g . c
 ( (C --> (RealPoset [.0,1.])) . c = RealPoset [.0,1.] & ff . c <<= gg . c ) by A1, A4, FUNCOP_1:7, WAYBEL_3:28;
hence  f . c <= g . c by Th3; ::_thesis: verum
end;
hence  ( ( for c being Element of C holds f . c <= g . c ) iff (C,f) @ <<= (C,g) @ ) by A2; ::_thesis: verum
end;

theorem :: LFUZZY_0:17
for C being non empty set
for s, t being Element of (FuzzyLattice C) holds
( s <<= t iff for c being Element of C holds (@ s) . c <= (@ t) . c )
proof
let C be non empty set ; ::_thesis: for s, t being Element of (FuzzyLattice C) holds
( s <<= t iff for c being Element of C holds (@ s) . c <= (@ t) . c )
let s, t be Element of (FuzzyLattice C); ::_thesis: ( s <<= t iff for c being Element of C holds (@ s) . c <= (@ t) . c )
 ( (C,(@ s)) @ = s & (C,(@ t)) @ = t ) ;
hence  ( s <<= t iff for c being Element of C holds (@ s) . c <= (@ t) . c ) by Th16; ::_thesis: verum
end;

theorem Th18: :: LFUZZY_0:18
for C being non empty set
for f, g being Membership_Func of C holds max (f,g) = ((C,f) @) "\/" ((C,g) @)
proof
let C be non empty set ; ::_thesis: for f, g being Membership_Func of C holds max (f,g) = ((C,f) @) "\/" ((C,g) @)
let f, g be Membership_Func of C; ::_thesis: max (f,g) = ((C,f) @) "\/" ((C,g) @)
set fg = ((C,f) @) "\/" ((C,g) @);
set R = RealPoset [.0,1.];
set J = C --> (RealPoset [.0,1.]);
A1: (RealPoset [.0,1.]) |^ C = product (C --> (RealPoset [.0,1.])) by YELLOW_1:def_5;
now__::_thesis:_for_c_being_Element_of_C_holds_(@_(((C,f)_@)_"\/"_((C,g)_@)))_._c_=_max_((f_._c),(g_._c))
let c be Element of C; ::_thesis: (@ (((C,f) @) "\/" ((C,g) @))) . c = max ((f . c),(g . c))
 ( ( for c being Element of C holds (C --> (RealPoset [.0,1.])) . c is sup-Semilattice ) & (C --> (RealPoset [.0,1.])) . c = RealPoset [.0,1.] ) by FUNCOP_1:7;
hence (@ (((C,f) @) "\/" ((C,g) @))) . c = (((C,f) @) . c) "\/" (((C,g) @) . c) by A1, Th12
.= max ((f . c),(g . c)) ;
::_thesis: verum
end;
hence  max (f,g) = ((C,f) @) "\/" ((C,g) @) by FUZZY_1:def_4; ::_thesis: verum
end;

theorem :: LFUZZY_0:19
for C being non empty set
for s, t being Element of (FuzzyLattice C) holds s "\/" t = max ((@ s),(@ t))
proof
let C be non empty set ; ::_thesis: for s, t being Element of (FuzzyLattice C) holds s "\/" t = max ((@ s),(@ t))
let s, t be Element of (FuzzyLattice C); ::_thesis: s "\/" t = max ((@ s),(@ t))
 ( (C,(@ s)) @ = s & (C,(@ t)) @ = t ) ;
hence  s "\/" t = max ((@ s),(@ t)) by Th18; ::_thesis: verum
end;

theorem Th20: :: LFUZZY_0:20
for C being non empty set
for f, g being Membership_Func of C holds min (f,g) = ((C,f) @) "/\" ((C,g) @)
proof
let C be non empty set ; ::_thesis: for f, g being Membership_Func of C holds min (f,g) = ((C,f) @) "/\" ((C,g) @)
let f, g be Membership_Func of C; ::_thesis: min (f,g) = ((C,f) @) "/\" ((C,g) @)
set fg = ((C,f) @) "/\" ((C,g) @);
set R = RealPoset [.0,1.];
set J = C --> (RealPoset [.0,1.]);
A1: (RealPoset [.0,1.]) |^ C = product (C --> (RealPoset [.0,1.])) by YELLOW_1:def_5;
now__::_thesis:_for_c_being_Element_of_C_holds_(@_(((C,f)_@)_"/\"_((C,g)_@)))_._c_=_min_((f_._c),(g_._c))
let c be Element of C; ::_thesis: (@ (((C,f) @) "/\" ((C,g) @))) . c = min ((f . c),(g . c))
 ( ( for c being Element of C holds (C --> (RealPoset [.0,1.])) . c is Semilattice ) & (C --> (RealPoset [.0,1.])) . c = RealPoset [.0,1.] ) by FUNCOP_1:7;
hence (@ (((C,f) @) "/\" ((C,g) @))) . c = (((C,f) @) . c) "/\" (((C,g) @) . c) by A1, Th11
.= min ((f . c),(g . c)) ;
::_thesis: verum
end;
hence  min (f,g) = ((C,f) @) "/\" ((C,g) @) by FUZZY_1:def_3; ::_thesis: verum
end;

theorem :: LFUZZY_0:21
for C being non empty set
for s, t being Element of (FuzzyLattice C) holds s "/\" t = min ((@ s),(@ t))
proof
let C be non empty set ; ::_thesis: for s, t being Element of (FuzzyLattice C) holds s "/\" t = min ((@ s),(@ t))
let s, t be Element of (FuzzyLattice C); ::_thesis: s "/\" t = min ((@ s),(@ t))
 ( (C,(@ s)) @ = s & (C,(@ t)) @ = t ) ;
hence  s "/\" t = min ((@ s),(@ t)) by Th20; ::_thesis: verum
end;

begin

scheme :: LFUZZY_0:sch 1
SupDistributivity{ F1() ->  complete LATTICE, F2() ->  non empty set , F3() ->  non empty set , F4( set , set ) ->  Element of F1(), P1[ set ], P2[ set ] } :
 "\/" ( {  ("\/" ( {  F4(x,y) where y is Element of F3() : P2[y]  }  ,F1())) where x is Element of F2() : P1[x]  }  ,F1()) = "\/" ( {  F4(x,y) where x is Element of F2(), y is Element of F3() : ( P1[x] & P2[y] )  }  ,F1())
proof
defpred S1[ set ] means  ex x being Element of F2() st
( P1[x] & ( for a being set holds
( a in $1 iff ex y being Element of F3() st
( a = F4(x,y) & P2[y] ) ) ) );
A1: "\/" ( {  ("\/" (A,F1())) where A is Subset of F1() : S1[A]  }  ,F1()) = "\/" ((union  {  A where A is Subset of F1() : S1[A]  }  ),F1()) from YELLOW_3:sch_5();
A2:  {  F4(x,y) where x is Element of F2(), y is Element of F3() : ( P1[x] & P2[y] )  }  c= union  {  A where A is Subset of F1() : S1[A]  }
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  F4(x,y) where x is Element of F2(), y is Element of F3() : ( P1[x] & P2[y] )  }  or a in union  {  A where A is Subset of F1() : S1[A]  }  )
assume  a in  {  F4(x,y) where x is Element of F2(), y is Element of F3() : ( P1[x] & P2[y] )  }  ; ::_thesis: a in union  {  A where A is Subset of F1() : S1[A]  }
then consider x being Element of F2(), y being Element of F3() such that
A3: a = F4(x,y) and
A4: P1[x] and
A5: P2[y] ;
set A1 =  {  F4(x,y9) where y9 is Element of F3() : P2[y9]  }  ;
  {  F4(x,y9) where y9 is Element of F3() : P2[y9]  }  c= the carrier of F1()
proof
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in  {  F4(x,y9) where y9 is Element of F3() : P2[y9]  }  or b in the carrier of F1() )
assume  b in  {  F4(x,y9) where y9 is Element of F3() : P2[y9]  }  ; ::_thesis: b in the carrier of F1()
then  ex y9 being Element of F3() st
( b = F4(x,y9) & P2[y9] ) ;
hence  b in the carrier of F1() ; ::_thesis: verum
end;
then reconsider A1 =  {  F4(x,y9) where y9 is Element of F3() : P2[y9]  }  as Subset of F1() ;
 S1[A1]
proof
take  x ; ::_thesis: ( P1[x] & ( for a being set holds
( a in A1 iff ex y being Element of F3() st
( a = F4(x,y) & P2[y] ) ) ) )
thus  P1[x] by A4; ::_thesis: for a being set holds
( a in A1 iff ex y being Element of F3() st
( a = F4(x,y) & P2[y] ) )
let a be set ; ::_thesis: ( a in A1 iff ex y being Element of F3() st
( a = F4(x,y) & P2[y] ) )
thus  ( a in A1 iff ex y being Element of F3() st
( a = F4(x,y) & P2[y] ) ) ; ::_thesis: verum
end;
then A6: A1 in  {  A where A is Subset of F1() : S1[A]  }  ;
 a in A1 by A3, A5;
hence  a in union  {  A where A is Subset of F1() : S1[A]  }  by A6, TARSKI:def_4; ::_thesis: verum
end;
A7:  {  ("\/" ( {  F4(x,y) where y is Element of F3() : P2[y]  }  ,F1())) where x is Element of F2() : P1[x]  }  c=  {  ("\/" (A,F1())) where A is Subset of F1() : S1[A]  }
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  ("\/" ( {  F4(x,y) where y is Element of F3() : P2[y]  }  ,F1())) where x is Element of F2() : P1[x]  }  or a in  {  ("\/" (A,F1())) where A is Subset of F1() : S1[A]  }  )
assume  a in  {  ("\/" ( {  F4(x,y) where y is Element of F3() : P2[y]  }  ,F1())) where x is Element of F2() : P1[x]  }  ; ::_thesis: a in  {  ("\/" (A,F1())) where A is Subset of F1() : S1[A]  }
then consider x being Element of F2() such that
A8: a = "\/" ( {  F4(x,y) where y is Element of F3() : P2[y]  }  ,F1()) and
A9: P1[x] ;
 ex A1 being Subset of F1() st
( a = "\/" (A1,F1()) & S1[A1] )
proof
set A2 =  {  F4(x,y) where y is Element of F3() : P2[y]  }  ;
  {  F4(x,y) where y is Element of F3() : P2[y]  }  c= the carrier of F1()
proof
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in  {  F4(x,y) where y is Element of F3() : P2[y]  }  or b in the carrier of F1() )
assume  b in  {  F4(x,y) where y is Element of F3() : P2[y]  }  ; ::_thesis: b in the carrier of F1()
then  ex y being Element of F3() st
( b = F4(x,y) & P2[y] ) ;
hence  b in the carrier of F1() ; ::_thesis: verum
end;
then reconsider A1 =  {  F4(x,y) where y is Element of F3() : P2[y]  }  as Subset of F1() ;
 S1[A1]
proof
take  x ; ::_thesis: ( P1[x] & ( for a being set holds
( a in A1 iff ex y being Element of F3() st
( a = F4(x,y) & P2[y] ) ) ) )
thus  P1[x] by A9; ::_thesis: for a being set holds
( a in A1 iff ex y being Element of F3() st
( a = F4(x,y) & P2[y] ) )
thus  for a being set holds
( a in A1 iff ex y being Element of F3() st
( a = F4(x,y) & P2[y] ) ) ; ::_thesis: verum
end;
hence  ex A1 being Subset of F1() st
( a = "\/" (A1,F1()) & S1[A1] ) by A8; ::_thesis: verum
end;
hence  a in  {  ("\/" (A,F1())) where A is Subset of F1() : S1[A]  }  ; ::_thesis: verum
end;
A10:  {  ("\/" (A,F1())) where A is Subset of F1() : S1[A]  }  c=  {  ("\/" ( {  F4(x,y) where y is Element of F3() : P2[y]  }  ,F1())) where x is Element of F2() : P1[x]  }
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  ("\/" (A,F1())) where A is Subset of F1() : S1[A]  }  or a in  {  ("\/" ( {  F4(x,y) where y is Element of F3() : P2[y]  }  ,F1())) where x is Element of F2() : P1[x]  }  )
assume  a in  {  ("\/" (A,F1())) where A is Subset of F1() : S1[A]  }  ; ::_thesis: a in  {  ("\/" ( {  F4(x,y) where y is Element of F3() : P2[y]  }  ,F1())) where x is Element of F2() : P1[x]  }
then consider A1 being Subset of F1() such that
A11: a = "\/" (A1,F1()) and
A12: S1[A1] ;
consider x being Element of F2() such that
A13: P1[x] and
A14: for a being set holds
( a in A1 iff ex y being Element of F3() st
( a = F4(x,y) & P2[y] ) ) by A12;
now__::_thesis:_for_a_being_set_holds_
(_a_in_A1_iff_a_in__{__F4(x,y)_where_y_is_Element_of_F3()_:_P2[y]__}__)
let a be set ; ::_thesis: ( a in A1 iff a in  {  F4(x,y) where y is Element of F3() : P2[y]  }  )
 ( a in  {  F4(x,y) where y is Element of F3() : P2[y]  }  iff ex y being Element of F3() st
( a = F4(x,y) & P2[y] ) ) ;
hence  ( a in A1 iff a in  {  F4(x,y) where y is Element of F3() : P2[y]  }  ) by A14; ::_thesis: verum
end;
then  A1 =  {  F4(x,y) where y is Element of F3() : P2[y]  }  by TARSKI:1;
hence  a in  {  ("\/" ( {  F4(x,y) where y is Element of F3() : P2[y]  }  ,F1())) where x is Element of F2() : P1[x]  }  by A11, A13; ::_thesis: verum
end;
 union  {  A where A is Subset of F1() : S1[A]  }  c=  {  F4(x,y) where x is Element of F2(), y is Element of F3() : ( P1[x] & P2[y] )  }
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in union  {  A where A is Subset of F1() : S1[A]  }  or a in  {  F4(x,y) where x is Element of F2(), y is Element of F3() : ( P1[x] & P2[y] )  }  )
assume  a in union  {  A where A is Subset of F1() : S1[A]  }  ; ::_thesis: a in  {  F4(x,y) where x is Element of F2(), y is Element of F3() : ( P1[x] & P2[y] )  }
then consider A1 being set  such that
A15: a in A1 and
A16: A1 in  {  A where A is Subset of F1() : S1[A]  }  by TARSKI:def_4;
consider A2 being Subset of F1() such that
A17: A1 = A2 and
A18: S1[A2] by A16;
consider x being Element of F2() such that
A19: P1[x] and
A20: for a being set holds
( a in A2 iff ex y being Element of F3() st
( a = F4(x,y) & P2[y] ) ) by A18;
 ex y being Element of F3() st
( a = F4(x,y) & P2[y] ) by A15, A17, A20;
hence  a in  {  F4(x,y) where x is Element of F2(), y is Element of F3() : ( P1[x] & P2[y] )  }  by A19; ::_thesis: verum
end;
then  union  {  A where A is Subset of F1() : S1[A]  }  =  {  F4(x,y) where x is Element of F2(), y is Element of F3() : ( P1[x] & P2[y] )  }  by A2, XBOOLE_0:def_10;
hence  "\/" ( {  ("\/" ( {  F4(x,y) where y is Element of F3() : P2[y]  }  ,F1())) where x is Element of F2() : P1[x]  }  ,F1()) = "\/" ( {  F4(x,y) where x is Element of F2(), y is Element of F3() : ( P1[x] & P2[y] )  }  ,F1()) by A1, A10, A7, XBOOLE_0:def_10; ::_thesis: verum
end;

scheme :: LFUZZY_0:sch 2
SupDistributivity9{ F1() ->  complete LATTICE, F2() ->  non empty set , F3() ->  non empty set , F4( set , set ) ->  Element of F1(), P1[ set ], P2[ set ] } :
 "\/" ( {  ("\/" ( {  F4(x,y) where x is Element of F2() : P1[x]  }  ,F1())) where y is Element of F3() : P2[y]  }  ,F1()) = "\/" ( {  F4(x,y) where x is Element of F2(), y is Element of F3() : ( P1[x] & P2[y] )  }  ,F1())
proof
defpred S1[ set ] means  ex y being Element of F3() st
( P2[y] & ( for a being set holds
( a in $1 iff ex x being Element of F2() st
( a = F4(x,y) & P1[x] ) ) ) );
A1: "\/" ( {  ("\/" (A,F1())) where A is Subset of F1() : S1[A]  }  ,F1()) = "\/" ((union  {  A where A is Subset of F1() : S1[A]  }  ),F1()) from YELLOW_3:sch_5();
A2:  {  F4(x,y) where x is Element of F2(), y is Element of F3() : ( P1[x] & P2[y] )  }  c= union  {  A where A is Subset of F1() : S1[A]  }
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  F4(x,y) where x is Element of F2(), y is Element of F3() : ( P1[x] & P2[y] )  }  or a in union  {  A where A is Subset of F1() : S1[A]  }  )
assume  a in  {  F4(x,y) where x is Element of F2(), y is Element of F3() : ( P1[x] & P2[y] )  }  ; ::_thesis: a in union  {  A where A is Subset of F1() : S1[A]  }
then consider x being Element of F2(), y being Element of F3() such that
A3: ( a = F4(x,y) & P1[x] ) and
A4: P2[y] ;
set A1 =  {  F4(x9,y) where x9 is Element of F2() : P1[x9]  }  ;
  {  F4(x9,y) where x9 is Element of F2() : P1[x9]  }  c= the carrier of F1()
proof
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in  {  F4(x9,y) where x9 is Element of F2() : P1[x9]  }  or b in the carrier of F1() )
assume  b in  {  F4(x9,y) where x9 is Element of F2() : P1[x9]  }  ; ::_thesis: b in the carrier of F1()
then  ex x9 being Element of F2() st
( b = F4(x9,y) & P1[x9] ) ;
hence  b in the carrier of F1() ; ::_thesis: verum
end;
then reconsider A1 =  {  F4(x9,y) where x9 is Element of F2() : P1[x9]  }  as Subset of F1() ;
 S1[A1]
proof
take  y ; ::_thesis: ( P2[y] & ( for a being set holds
( a in A1 iff ex x being Element of F2() st
( a = F4(x,y) & P1[x] ) ) ) )
thus  P2[y] by A4; ::_thesis: for a being set holds
( a in A1 iff ex x being Element of F2() st
( a = F4(x,y) & P1[x] ) )
let a be set ; ::_thesis: ( a in A1 iff ex x being Element of F2() st
( a = F4(x,y) & P1[x] ) )
thus  ( a in A1 iff ex x being Element of F2() st
( a = F4(x,y) & P1[x] ) ) ; ::_thesis: verum
end;
then A5: A1 in  {  A where A is Subset of F1() : S1[A]  }  ;
 a in A1 by A3;
hence  a in union  {  A where A is Subset of F1() : S1[A]  }  by A5, TARSKI:def_4; ::_thesis: verum
end;
A6:  {  ("\/" ( {  F4(x,y) where x is Element of F2() : P1[x]  }  ,F1())) where y is Element of F3() : P2[y]  }  c=  {  ("\/" (A,F1())) where A is Subset of F1() : S1[A]  }
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  ("\/" ( {  F4(x,y) where x is Element of F2() : P1[x]  }  ,F1())) where y is Element of F3() : P2[y]  }  or a in  {  ("\/" (A,F1())) where A is Subset of F1() : S1[A]  }  )
assume  a in  {  ("\/" ( {  F4(x,y) where x is Element of F2() : P1[x]  }  ,F1())) where y is Element of F3() : P2[y]  }  ; ::_thesis: a in  {  ("\/" (A,F1())) where A is Subset of F1() : S1[A]  }
then consider y being Element of F3() such that
A7: a = "\/" ( {  F4(x,y) where x is Element of F2() : P1[x]  }  ,F1()) and
A8: P2[y] ;
 ex A1 being Subset of F1() st
( a = "\/" (A1,F1()) & S1[A1] )
proof
set A2 =  {  F4(x,y) where x is Element of F2() : P1[x]  }  ;
  {  F4(x,y) where x is Element of F2() : P1[x]  }  c= the carrier of F1()
proof
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in  {  F4(x,y) where x is Element of F2() : P1[x]  }  or b in the carrier of F1() )
assume  b in  {  F4(x,y) where x is Element of F2() : P1[x]  }  ; ::_thesis: b in the carrier of F1()
then  ex x being Element of F2() st
( b = F4(x,y) & P1[x] ) ;
hence  b in the carrier of F1() ; ::_thesis: verum
end;
then reconsider A1 =  {  F4(x,y) where x is Element of F2() : P1[x]  }  as Subset of F1() ;
 S1[A1]
proof
take  y ; ::_thesis: ( P2[y] & ( for a being set holds
( a in A1 iff ex x being Element of F2() st
( a = F4(x,y) & P1[x] ) ) ) )
thus  P2[y] by A8; ::_thesis: for a being set holds
( a in A1 iff ex x being Element of F2() st
( a = F4(x,y) & P1[x] ) )
thus  for a being set holds
( a in A1 iff ex x being Element of F2() st
( a = F4(x,y) & P1[x] ) ) ; ::_thesis: verum
end;
hence  ex A1 being Subset of F1() st
( a = "\/" (A1,F1()) & S1[A1] ) by A7; ::_thesis: verum
end;
hence  a in  {  ("\/" (A,F1())) where A is Subset of F1() : S1[A]  }  ; ::_thesis: verum
end;
A9:  {  ("\/" (A,F1())) where A is Subset of F1() : S1[A]  }  c=  {  ("\/" ( {  F4(x,y) where x is Element of F2() : P1[x]  }  ,F1())) where y is Element of F3() : P2[y]  }
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  ("\/" (A,F1())) where A is Subset of F1() : S1[A]  }  or a in  {  ("\/" ( {  F4(x,y) where x is Element of F2() : P1[x]  }  ,F1())) where y is Element of F3() : P2[y]  }  )
assume  a in  {  ("\/" (A,F1())) where A is Subset of F1() : S1[A]  }  ; ::_thesis: a in  {  ("\/" ( {  F4(x,y) where x is Element of F2() : P1[x]  }  ,F1())) where y is Element of F3() : P2[y]  }
then consider A1 being Subset of F1() such that
A10: a = "\/" (A1,F1()) and
A11: S1[A1] ;
consider y being Element of F3() such that
A12: P2[y] and
A13: for a being set holds
( a in A1 iff ex x being Element of F2() st
( a = F4(x,y) & P1[x] ) ) by A11;
now__::_thesis:_for_a_being_set_holds_
(_a_in_A1_iff_a_in__{__F4(x,y)_where_x_is_Element_of_F2()_:_P1[x]__}__)
let a be set ; ::_thesis: ( a in A1 iff a in  {  F4(x,y) where x is Element of F2() : P1[x]  }  )
 ( a in  {  F4(x,y) where x is Element of F2() : P1[x]  }  iff ex x being Element of F2() st
( a = F4(x,y) & P1[x] ) ) ;
hence  ( a in A1 iff a in  {  F4(x,y) where x is Element of F2() : P1[x]  }  ) by A13; ::_thesis: verum
end;
then  A1 =  {  F4(x,y) where x is Element of F2() : P1[x]  }  by TARSKI:1;
hence  a in  {  ("\/" ( {  F4(x,y) where x is Element of F2() : P1[x]  }  ,F1())) where y is Element of F3() : P2[y]  }  by A10, A12; ::_thesis: verum
end;
 union  {  A where A is Subset of F1() : S1[A]  }  c=  {  F4(x,y) where x is Element of F2(), y is Element of F3() : ( P1[x] & P2[y] )  }
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in union  {  A where A is Subset of F1() : S1[A]  }  or a in  {  F4(x,y) where x is Element of F2(), y is Element of F3() : ( P1[x] & P2[y] )  }  )
assume  a in union  {  A where A is Subset of F1() : S1[A]  }  ; ::_thesis: a in  {  F4(x,y) where x is Element of F2(), y is Element of F3() : ( P1[x] & P2[y] )  }
then consider A1 being set  such that
A14: a in A1 and
A15: A1 in  {  A where A is Subset of F1() : S1[A]  }  by TARSKI:def_4;
consider A2 being Subset of F1() such that
A16: A1 = A2 and
A17: S1[A2] by A15;
consider y being Element of F3() such that
A18: P2[y] and
A19: for a being set holds
( a in A2 iff ex x being Element of F2() st
( a = F4(x,y) & P1[x] ) ) by A17;
 ex x being Element of F2() st
( a = F4(x,y) & P1[x] ) by A14, A16, A19;
hence  a in  {  F4(x,y) where x is Element of F2(), y is Element of F3() : ( P1[x] & P2[y] )  }  by A18; ::_thesis: verum
end;
then  union  {  A where A is Subset of F1() : S1[A]  }  =  {  F4(x,y) where x is Element of F2(), y is Element of F3() : ( P1[x] & P2[y] )  }  by A2, XBOOLE_0:def_10;
hence  "\/" ( {  ("\/" ( {  F4(x,y) where x is Element of F2() : P1[x]  }  ,F1())) where y is Element of F3() : P2[y]  }  ,F1()) = "\/" ( {  F4(x,y) where x is Element of F2(), y is Element of F3() : ( P1[x] & P2[y] )  }  ,F1()) by A1, A9, A6, XBOOLE_0:def_10; ::_thesis: verum
end;

scheme :: LFUZZY_0:sch 3
FraenkelF9R9{ F1() ->  non empty set , F2() ->  non empty set , F3( set , set ) ->  set , F4( set , set ) ->  set , P1[ set , set ] } :
  {  F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1]  }  =  {  F4(u2,v2) where u2 is Element of F1(), v2 is Element of F2() : P1[u2,v2]  }
provided
A1: for u being Element of F1()
for v being Element of F2() st P1[u,v] holds
F3(u,v) = F4(u,v)
proof
set A =  {  F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1]  }  ;
set C =  {  F4(u3,v3) where u3 is Element of F1(), v3 is Element of F2() : P1[u3,v3]  }  ;
 for a being set holds
( a in  {  F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1]  }  iff a in  {  F4(u3,v3) where u3 is Element of F1(), v3 is Element of F2() : P1[u3,v3]  }  )
proof
let a be set ; ::_thesis: ( a in  {  F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1]  }  iff a in  {  F4(u3,v3) where u3 is Element of F1(), v3 is Element of F2() : P1[u3,v3]  }  )
hereby  ::_thesis: ( a in  {  F4(u3,v3) where u3 is Element of F1(), v3 is Element of F2() : P1[u3,v3]  }  implies a in  {  F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1]  }  )
assume  a in  {  F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1]  }  ; ::_thesis: a in  {  F4(u3,v3) where u3 is Element of F1(), v3 is Element of F2() : P1[u3,v3]  }
then consider u being Element of F1(), v being Element of F2() such that
A2: a = F3(u,v) and
A3: P1[u,v] ;
 a = F4(u,v) by A1, A2, A3;
hence  a in  {  F4(u3,v3) where u3 is Element of F1(), v3 is Element of F2() : P1[u3,v3]  }  by A3; ::_thesis: verum
end;
assume  a in  {  F4(u3,v3) where u3 is Element of F1(), v3 is Element of F2() : P1[u3,v3]  }  ; ::_thesis: a in  {  F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1]  }
then consider u being Element of F1(), v being Element of F2() such that
A4: a = F4(u,v) and
A5: P1[u,v] ;
 a = F3(u,v) by A1, A4, A5;
hence  a in  {  F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1]  }  by A5; ::_thesis: verum
end;
hence   {  F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1]  }  =  {  F4(u2,v2) where u2 is Element of F1(), v2 is Element of F2() : P1[u2,v2]  }  by TARSKI:1; ::_thesis: verum
end;

scheme :: LFUZZY_0:sch 4
FraenkelF699R{ F1() ->  non empty set , F2() ->  non empty set , F3( set , set ) ->  set , F4( set , set ) ->  set , P1[ set , set ], P2[ set , set ] } :
  {  F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1]  }  =  {  F4(u2,v2) where u2 is Element of F1(), v2 is Element of F2() : P2[u2,v2]  }
provided
A1: for u being Element of F1()
for v being Element of F2() holds
( P1[u,v] iff P2[u,v] ) and
A2: for u being Element of F1()
for v being Element of F2() st P1[u,v] holds
F3(u,v) = F4(u,v)
proof
set A =  {  F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1]  }  ;
set B =  {  F4(u2,v2) where u2 is Element of F1(), v2 is Element of F2() : P2[u2,v2]  }  ;
set C =  {  F4(u3,v3) where u3 is Element of F1(), v3 is Element of F2() : P1[u3,v3]  }  ;
A3:  {  F4(u3,v3) where u3 is Element of F1(), v3 is Element of F2() : P1[u3,v3]  }  =  {  F4(u2,v2) where u2 is Element of F1(), v2 is Element of F2() : P2[u2,v2]  }  from FRAENKEL:sch_4(A1);
  {  F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1]  }  =  {  F4(u3,v3) where u3 is Element of F1(), v3 is Element of F2() : P1[u3,v3]  }  from LFUZZY_0:sch_3(A2);
hence   {  F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1]  }  =  {  F4(u2,v2) where u2 is Element of F1(), v2 is Element of F2() : P2[u2,v2]  }  by A3; ::_thesis: verum
end;

scheme :: LFUZZY_0:sch 5
SupCommutativity{ F1() ->  complete LATTICE, F2() ->  non empty set , F3() ->  non empty set , F4( set , set ) ->  Element of F1(), F5( set , set ) ->  Element of F1(), P1[ set ], P2[ set ] } :
 "\/" ( {  ("\/" ( {  F4(x,y) where y is Element of F3() : P2[y]  }  ,F1())) where x is Element of F2() : P1[x]  }  ,F1()) = "\/" ( {  ("\/" ( {  F5(x9,y9) where x9 is Element of F2() : P1[x9]  }  ,F1())) where y9 is Element of F3() : P2[y9]  }  ,F1())
provided
A1: for x being Element of F2()
for y being Element of F3() st P1[x] & P2[y] holds
F4(x,y) = F5(x,y)
proof
defpred S1[ set , set ] means ( P1[$1] & P2[$2] );
A2: for x being Element of F2()
for y being Element of F3() holds
( S1[x,y] iff S1[x,y] ) ;
A3: for x being Element of F2()
for y being Element of F3() st S1[x,y] holds
F4(x,y) = F5(x,y) by A1;
A4:  {  F4(x9,y9) where x9 is Element of F2(), y9 is Element of F3() : S1[x9,y9]  }  =  {  F5(x,y) where x is Element of F2(), y is Element of F3() : S1[x,y]  }  from LFUZZY_0:sch_4(A2, A3);
A5: "\/" ( {  ("\/" ( {  F4(x,y) where y is Element of F3() : P2[y]  }  ,F1())) where x is Element of F2() : P1[x]  }  ,F1()) = "\/" ( {  F4(x,y) where x is Element of F2(), y is Element of F3() : ( P1[x] & P2[y] )  }  ,F1()) from LFUZZY_0:sch_1();
"\/" ( {  ("\/" ( {  F5(x9,y9) where x9 is Element of F2() : P1[x9]  }  ,F1())) where y9 is Element of F3() : P2[y9]  }  ,F1()) = "\/" ( {  F5(x9,y9) where x9 is Element of F2(), y9 is Element of F3() : ( P1[x9] & P2[y9] )  }  ,F1()) from LFUZZY_0:sch_2()
.= "\/" ( {  F4(x9,y9) where x9 is Element of F2(), y9 is Element of F3() : ( P1[x9] & P2[y9] )  }  ,F1()) by A4 ;
hence  "\/" ( {  ("\/" ( {  F4(x,y) where y is Element of F3() : P2[y]  }  ,F1())) where x is Element of F2() : P1[x]  }  ,F1()) = "\/" ( {  ("\/" ( {  F5(x9,y9) where x9 is Element of F2() : P1[x9]  }  ,F1())) where y9 is Element of F3() : P2[y9]  }  ,F1()) by A5; ::_thesis: verum
end;

Lm4:  for x being Element of (RealPoset [.0,1.]) holds x is Real
proof
let x be Element of (RealPoset [.0,1.]); ::_thesis: x is Real
 ( x in the carrier of (RealPoset [.0,1.]) & the carrier of (RealPoset [.0,1.]) = [.0,1.] ) by Def3;
hence  x is Real ; ::_thesis: verum
end;

Lm5:  for X, Y, Z being non empty set
for R being RMembership_Func of X,Y
for S being RMembership_Func of Y,Z
for x being Element of X
for z being Element of Z holds
( rng (min (R,S,x,z)) =  {  ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum  }  & rng (min (R,S,x,z)) <> {} )
proof
let X, Y, Z be non empty set ; ::_thesis: for R being RMembership_Func of X,Y
for S being RMembership_Func of Y,Z
for x being Element of X
for z being Element of Z holds
( rng (min (R,S,x,z)) =  {  ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum  }  & rng (min (R,S,x,z)) <> {} )
let R be RMembership_Func of X,Y; ::_thesis: for S being RMembership_Func of Y,Z
for x being Element of X
for z being Element of Z holds
( rng (min (R,S,x,z)) =  {  ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum  }  & rng (min (R,S,x,z)) <> {} )
let S be RMembership_Func of Y,Z; ::_thesis: for x being Element of X
for z being Element of Z holds
( rng (min (R,S,x,z)) =  {  ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum  }  & rng (min (R,S,x,z)) <> {} )
let x be Element of X; ::_thesis: for z being Element of Z holds
( rng (min (R,S,x,z)) =  {  ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum  }  & rng (min (R,S,x,z)) <> {} )
let z be Element of Z; ::_thesis: ( rng (min (R,S,x,z)) =  {  ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum  }  & rng (min (R,S,x,z)) <> {} )
set L =  {  ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum  }  ;
A1: ( Y = dom (min (R,S,x,z)) & min (R,S,x,z) is PartFunc of (dom (min (R,S,x,z))),(rng (min (R,S,x,z))) ) by FUNCT_2:def_1, RELSET_1:4;
 for c being set holds
( c in  {  ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum  }  iff c in rng (min (R,S,x,z)) )
proof
let c be set ; ::_thesis: ( c in  {  ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum  }  iff c in rng (min (R,S,x,z)) )
hereby  ::_thesis: ( c in rng (min (R,S,x,z)) implies c in  {  ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum  }  )
assume  c in  {  ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum  }  ; ::_thesis: c in rng (min (R,S,x,z))
then consider y being Element of Y such that
A2: c = (R . (x,y)) "/\" (S . (y,z)) ;
 c = (min (R,S,x,z)) . y by A2, FUZZY_4:def_2;
hence  c in rng (min (R,S,x,z)) by A1, PARTFUN1:4; ::_thesis: verum
end;
assume  c in rng (min (R,S,x,z)) ; ::_thesis: c in  {  ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum  }
then consider y being Element of Y such that
 y in dom (min (R,S,x,z)) and
A3: c = (min (R,S,x,z)) . y by PARTFUN1:3;
 c = (R . (x,y)) "/\" (S . (y,z)) by A3, FUZZY_4:def_2;
hence  c in  {  ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum  }  ; ::_thesis: verum
end;
hence  rng (min (R,S,x,z)) =  {  ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum  }  by TARSKI:1; ::_thesis: rng (min (R,S,x,z)) <> {}
 ex d being set st d in rng (min (R,S,x,z))
proof
set y = the Element of Y;
take  (min (R,S,x,z)) . the Element of Y ; ::_thesis: (min (R,S,x,z)) . the Element of Y in rng (min (R,S,x,z))
thus  (min (R,S,x,z)) . the Element of Y in rng (min (R,S,x,z)) by A1, PARTFUN1:4; ::_thesis: verum
end;
hence  rng (min (R,S,x,z)) <> {} ; ::_thesis: verum
end;

theorem Th22: :: LFUZZY_0:22
for X, Y, Z being non empty set
for R being RMembership_Func of X,Y
for S being RMembership_Func of Y,Z
for x being Element of X
for z being Element of Z holds (R (#) S) . (x,z) = "\/" ( {  ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum  }  ,(RealPoset [.0,1.]))
proof
let X, Y, Z be non empty set ; ::_thesis: for R being RMembership_Func of X,Y
for S being RMembership_Func of Y,Z
for x being Element of X
for z being Element of Z holds (R (#) S) . (x,z) = "\/" ( {  ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum  }  ,(RealPoset [.0,1.]))
let R be RMembership_Func of X,Y; ::_thesis: for S being RMembership_Func of Y,Z
for x being Element of X
for z being Element of Z holds (R (#) S) . (x,z) = "\/" ( {  ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum  }  ,(RealPoset [.0,1.]))
let S be RMembership_Func of Y,Z; ::_thesis: for x being Element of X
for z being Element of Z holds (R (#) S) . (x,z) = "\/" ( {  ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum  }  ,(RealPoset [.0,1.]))
let x be Element of X; ::_thesis: for z being Element of Z holds (R (#) S) . (x,z) = "\/" ( {  ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum  }  ,(RealPoset [.0,1.]))
let z be Element of Z; ::_thesis: (R (#) S) . (x,z) = "\/" ( {  ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum  }  ,(RealPoset [.0,1.]))
set L =  {  ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum  }  ;
 [x,z] in [:X,Z:] ;
then A1: (R (#) S) . (x,z) = upper_bound (rng (min (R,S,x,z))) by FUZZY_4:def_3;
A2: for b being Element of (RealPoset [.0,1.]) st b is_>=_than  {  ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum  }  holds
(R (#) S) . (x,z) <<= b
proof
let b be Element of (RealPoset [.0,1.]); ::_thesis: ( b is_>=_than  {  ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum  }  implies (R (#) S) . (x,z) <<= b )
assume A3: b is_>=_than  {  ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum  }  ; ::_thesis: (R (#) S) . (x,z) <<= b
A4: rng (min (R,S,x,z)) c= [.0,1.] by RELAT_1:def_19;
A5:  {  ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum  }  = rng (min (R,S,x,z)) by Lm5;
A6: for r being real number st r in rng (min (R,S,x,z)) holds
r <= b
proof
let r be real number ; ::_thesis: ( r in rng (min (R,S,x,z)) implies r <= b )
assume A7: r in rng (min (R,S,x,z)) ; ::_thesis: r <= b
then reconsider r = r as Element of (RealPoset [.0,1.]) by A4, Def3;
 r <<= b by A3, A5, A7, LATTICE3:def_9;
hence  r <= b by Th3; ::_thesis: verum
end;
 rng (min (R,S,x,z)) <> {} by Lm5;
then  upper_bound (rng (min (R,S,x,z))) <= b by A6, SEQ_4:144;
hence  (R (#) S) . (x,z) <<= b by A1, Th3; ::_thesis: verum
end;
 for b being Element of (RealPoset [.0,1.]) st b in  {  ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum  }  holds
(R (#) S) . [x,z] >>= b
proof
let b be Element of (RealPoset [.0,1.]); ::_thesis: ( b in  {  ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum  }  implies (R (#) S) . [x,z] >>= b )
assume  b in  {  ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum  }  ; ::_thesis: (R (#) S) . [x,z] >>= b
then consider y being Element of Y such that
A8: b = (R . (x,y)) "/\" (S . (y,z)) and
 verum ;
reconsider b = b as Real by Lm4;
 ( dom (min (R,S,x,z)) = Y & b = (min (R,S,x,z)) . y ) by A8, FUNCT_2:def_1, FUZZY_4:def_2;
then  b <= upper_bound (rng (min (R,S,x,z))) by FUZZY_4:1;
hence  (R (#) S) . [x,z] >>= b by A1, Th3; ::_thesis: verum
end;
then  (R (#) S) . [x,z] is_>=_than  {  ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum  }  by LATTICE3:def_9;
hence  (R (#) S) . (x,z) = "\/" ( {  ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum  }  ,(RealPoset [.0,1.])) by A2, YELLOW_0:32; ::_thesis: verum
end;

Lm6:  for X, Y, Z being non empty set
for R being RMembership_Func of X,Y
for S being RMembership_Func of Y,Z
for x being Element of X
for z being Element of Z
for a being Element of (RealPoset [.0,1.]) holds ((R (#) S) . (x,z)) "/\" a = "\/" ( {  (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum  }  ,(RealPoset [.0,1.]))
proof
let X, Y, Z be non empty set ; ::_thesis: for R being RMembership_Func of X,Y
for S being RMembership_Func of Y,Z
for x being Element of X
for z being Element of Z
for a being Element of (RealPoset [.0,1.]) holds ((R (#) S) . (x,z)) "/\" a = "\/" ( {  (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum  }  ,(RealPoset [.0,1.]))
let R be RMembership_Func of X,Y; ::_thesis: for S being RMembership_Func of Y,Z
for x being Element of X
for z being Element of Z
for a being Element of (RealPoset [.0,1.]) holds ((R (#) S) . (x,z)) "/\" a = "\/" ( {  (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum  }  ,(RealPoset [.0,1.]))
let S be RMembership_Func of Y,Z; ::_thesis: for x being Element of X
for z being Element of Z
for a being Element of (RealPoset [.0,1.]) holds ((R (#) S) . (x,z)) "/\" a = "\/" ( {  (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum  }  ,(RealPoset [.0,1.]))
let x be Element of X; ::_thesis: for z being Element of Z
for a being Element of (RealPoset [.0,1.]) holds ((R (#) S) . (x,z)) "/\" a = "\/" ( {  (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum  }  ,(RealPoset [.0,1.]))
let z be Element of Z; ::_thesis: for a being Element of (RealPoset [.0,1.]) holds ((R (#) S) . (x,z)) "/\" a = "\/" ( {  (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum  }  ,(RealPoset [.0,1.]))
let a be Element of (RealPoset [.0,1.]); ::_thesis: ((R (#) S) . (x,z)) "/\" a = "\/" ( {  (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum  }  ,(RealPoset [.0,1.]))
A1:  {  ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum  }  c= the carrier of (RealPoset [.0,1.])
proof
let d be set ; :: according to TARSKI:def_3 ::_thesis: ( not d in  {  ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum  }  or d in the carrier of (RealPoset [.0,1.]) )
assume  d in  {  ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum  }  ; ::_thesis: d in the carrier of (RealPoset [.0,1.])
then  ex t being Element of Y st d = (R . (x,t)) "/\" (S . (t,z)) ;
hence  d in the carrier of (RealPoset [.0,1.]) ; ::_thesis: verum
end;
set A =  {  (b "/\" a) where b is Element of (RealPoset [.0,1.]) : b in  {  ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum  }   }  ;
set B =  {  (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum  }  ;
A2: for c being set holds
( c in  {  (b "/\" a) where b is Element of (RealPoset [.0,1.]) : b in  {  ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum  }   }  iff c in  {  (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum  }  )
proof
let c be set ; ::_thesis: ( c in  {  (b "/\" a) where b is Element of (RealPoset [.0,1.]) : b in  {  ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum  }   }  iff c in  {  (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum  }  )
hereby  ::_thesis: ( c in  {  (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum  }  implies c in  {  (b "/\" a) where b is Element of (RealPoset [.0,1.]) : b in  {  ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum  }   }  )
assume  c in  {  (b "/\" a) where b is Element of (RealPoset [.0,1.]) : b in  {  ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum  }   }  ; ::_thesis: c in  {  (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum  }
then consider b being Element of (RealPoset [.0,1.]) such that
A3: c = b "/\" a and
A4: b in  {  ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum  }  ;
 ex y being Element of Y st b = (R . (x,y)) "/\" (S . (y,z)) by A4;
hence  c in  {  (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum  }  by A3; ::_thesis: verum
end;
assume  c in  {  (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum  }  ; ::_thesis: c in  {  (b "/\" a) where b is Element of (RealPoset [.0,1.]) : b in  {  ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum  }   }
then consider y being Element of Y such that
A5: c = ((R . (x,y)) "/\" (S . (y,z))) "/\" a ;
 (R . (x,y)) "/\" (S . (y,z)) in  {  ((R . (x,y1)) "/\" (S . (y1,z))) where y1 is Element of Y : verum  }  ;
hence  c in  {  (b "/\" a) where b is Element of (RealPoset [.0,1.]) : b in  {  ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum  }   }  by A5; ::_thesis: verum
end;
((R (#) S) . (x,z)) "/\" a = ("\/" ( {  ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum  }  ,(RealPoset [.0,1.]))) "/\" a by Th22
.= "\/" ( {  (b "/\" a) where b is Element of (RealPoset [.0,1.]) : b in  {  ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum  }   }  ,(RealPoset [.0,1.])) by A1, Th15 ;
hence  ((R (#) S) . (x,z)) "/\" a = "\/" ( {  (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum  }  ,(RealPoset [.0,1.])) by A2, TARSKI:1; ::_thesis: verum
end;

Lm7:  for X, Y, Z being non empty set
for R being RMembership_Func of X,Y
for S being RMembership_Func of Y,Z
for x being Element of X
for z being Element of Z
for a being Element of (RealPoset [.0,1.]) holds a "/\" ((R (#) S) . (x,z)) = "\/" ( {  ((a "/\" (R . (x,y))) "/\" (S . (y,z))) where y is Element of Y : verum  }  ,(RealPoset [.0,1.]))
proof
let X, Y, Z be non empty set ; ::_thesis: for R being RMembership_Func of X,Y
for S being RMembership_Func of Y,Z
for x being Element of X
for z being Element of Z
for a being Element of (RealPoset [.0,1.]) holds a "/\" ((R (#) S) . (x,z)) = "\/" ( {  ((a "/\" (R . (x,y))) "/\" (S . (y,z))) where y is Element of Y : verum  }  ,(RealPoset [.0,1.]))
let R be RMembership_Func of X,Y; ::_thesis: for S being RMembership_Func of Y,Z
for x being Element of X
for z being Element of Z
for a being Element of (RealPoset [.0,1.]) holds a "/\" ((R (#) S) . (x,z)) = "\/" ( {  ((a "/\" (R . (x,y))) "/\" (S . (y,z))) where y is Element of Y : verum  }  ,(RealPoset [.0,1.]))
let S be RMembership_Func of Y,Z; ::_thesis: for x being Element of X
for z being Element of Z
for a being Element of (RealPoset [.0,1.]) holds a "/\" ((R (#) S) . (x,z)) = "\/" ( {  ((a "/\" (R . (x,y))) "/\" (S . (y,z))) where y is Element of Y : verum  }  ,(RealPoset [.0,1.]))
let x be Element of X; ::_thesis: for z being Element of Z
for a being Element of (RealPoset [.0,1.]) holds a "/\" ((R (#) S) . (x,z)) = "\/" ( {  ((a "/\" (R . (x,y))) "/\" (S . (y,z))) where y is Element of Y : verum  }  ,(RealPoset [.0,1.]))
let z be Element of Z; ::_thesis: for a being Element of (RealPoset [.0,1.]) holds a "/\" ((R (#) S) . (x,z)) = "\/" ( {  ((a "/\" (R . (x,y))) "/\" (S . (y,z))) where y is Element of Y : verum  }  ,(RealPoset [.0,1.]))
let a be Element of (RealPoset [.0,1.]); ::_thesis: a "/\" ((R (#) S) . (x,z)) = "\/" ( {  ((a "/\" (R . (x,y))) "/\" (S . (y,z))) where y is Element of Y : verum  }  ,(RealPoset [.0,1.]))
set A =  {  ((a "/\" (R . (x,y))) "/\" (S . (y,z))) where y is Element of Y : verum  }  ;
set B =  {  (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum  }  ;
 for b being set holds
( b in  {  ((a "/\" (R . (x,y))) "/\" (S . (y,z))) where y is Element of Y : verum  }  iff b in  {  (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum  }  )
proof
let b be set ; ::_thesis: ( b in  {  ((a "/\" (R . (x,y))) "/\" (S . (y,z))) where y is Element of Y : verum  }  iff b in  {  (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum  }  )
hereby  ::_thesis: ( b in  {  (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum  }  implies b in  {  ((a "/\" (R . (x,y))) "/\" (S . (y,z))) where y is Element of Y : verum  }  )
assume  b in  {  ((a "/\" (R . (x,y))) "/\" (S . (y,z))) where y is Element of Y : verum  }  ; ::_thesis: b in  {  (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum  }
then consider y being Element of Y such that
A1: b = (a "/\" (R . (x,y))) "/\" (S . (y,z)) ;
 b = ((R . (x,y)) "/\" (S . (y,z))) "/\" a by A1, LATTICE3:16;
hence  b in  {  (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum  }  ; ::_thesis: verum
end;
assume  b in  {  (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum  }  ; ::_thesis: b in  {  ((a "/\" (R . (x,y))) "/\" (S . (y,z))) where y is Element of Y : verum  }
then consider y being Element of Y such that
A2: b = ((R . (x,y)) "/\" (S . (y,z))) "/\" a ;
 b = (a "/\" (R . (x,y))) "/\" (S . (y,z)) by A2, LATTICE3:16;
hence  b in  {  ((a "/\" (R . (x,y))) "/\" (S . (y,z))) where y is Element of Y : verum  }  ; ::_thesis: verum
end;
then   {  ((a "/\" (R . (x,y))) "/\" (S . (y,z))) where y is Element of Y : verum  }  =  {  (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum  }  by TARSKI:1;
hence  a "/\" ((R (#) S) . (x,z)) = "\/" ( {  ((a "/\" (R . (x,y))) "/\" (S . (y,z))) where y is Element of Y : verum  }  ,(RealPoset [.0,1.])) by Lm6; ::_thesis: verum
end;

theorem :: LFUZZY_0:23
for X, Y, Z, W being non empty set
for R being RMembership_Func of X,Y
for S being RMembership_Func of Y,Z
for T being RMembership_Func of Z,W holds (R (#) S) (#) T = R (#) (S (#) T)
proof
let X, Y, Z, W be non empty set ; ::_thesis: for R being RMembership_Func of X,Y
for S being RMembership_Func of Y,Z
for T being RMembership_Func of Z,W holds (R (#) S) (#) T = R (#) (S (#) T)
let R be RMembership_Func of X,Y; ::_thesis: for S being RMembership_Func of Y,Z
for T being RMembership_Func of Z,W holds (R (#) S) (#) T = R (#) (S (#) T)
let S be RMembership_Func of Y,Z; ::_thesis: for T being RMembership_Func of Z,W holds (R (#) S) (#) T = R (#) (S (#) T)
let T be RMembership_Func of Z,W; ::_thesis: (R (#) S) (#) T = R (#) (S (#) T)
A1: for x, w being set st x in X & w in W holds
((R (#) S) (#) T) . (x,w) = (R (#) (S (#) T)) . (x,w)
proof
let x, w be set ; ::_thesis: ( x in X & w in W implies ((R (#) S) (#) T) . (x,w) = (R (#) (S (#) T)) . (x,w) )
assume that
A2: x in X and
A3: w in W ; ::_thesis: ((R (#) S) (#) T) . (x,w) = (R (#) (S (#) T)) . (x,w)
reconsider w = w as Element of W by A3;
reconsider x = x as Element of X by A2;
set A =  {  ("\/" ( {  (((R . (x,y)) "/\" (S . (y,z))) "/\" (T . (z,w))) where y is Element of Y : verum  }  ,(RealPoset [.0,1.]))) where z is Element of Z : verum  }  ;
set B =  {  (((R (#) S) . (x,z)) "/\" (T . (z,w))) where z is Element of Z : verum  }  ;
set C =  {  ("\/" ( {  (((R . (x,y)) "/\" (S . (y,z))) "/\" (T . (z,w))) where z is Element of Z : verum  }  ,(RealPoset [.0,1.]))) where y is Element of Y : verum  }  ;
set D =  {  ((R . (x,y)) "/\" ((S (#) T) . (y,w))) where y is Element of Y : verum  }  ;
defpred S1[ set ] means verum;
deffunc H1( Element of Y, Element of Z) ->  Element of the carrier of (RealPoset [.0,1.]) = ((R . (x,$1)) "/\" (S . ($1,$2))) "/\" (T . ($2,w));
A4: for a being set holds
( a in  {  ("\/" ( {  (((R . (x,y)) "/\" (S . (y,z))) "/\" (T . (z,w))) where y is Element of Y : verum  }  ,(RealPoset [.0,1.]))) where z is Element of Z : verum  }  iff a in  {  (((R (#) S) . (x,z)) "/\" (T . (z,w))) where z is Element of Z : verum  }  )
proof
let a be set ; ::_thesis: ( a in  {  ("\/" ( {  (((R . (x,y)) "/\" (S . (y,z))) "/\" (T . (z,w))) where y is Element of Y : verum  }  ,(RealPoset [.0,1.]))) where z is Element of Z : verum  }  iff a in  {  (((R (#) S) . (x,z)) "/\" (T . (z,w))) where z is Element of Z : verum  }  )
hereby  ::_thesis: ( a in  {  (((R (#) S) . (x,z)) "/\" (T . (z,w))) where z is Element of Z : verum  }  implies a in  {  ("\/" ( {  (((R . (x,y)) "/\" (S . (y,z))) "/\" (T . (z,w))) where y is Element of Y : verum  }  ,(RealPoset [.0,1.]))) where z is Element of Z : verum  }  )
assume  a in  {  ("\/" ( {  (((R . (x,y)) "/\" (S . (y,z))) "/\" (T . (z,w))) where y is Element of Y : verum  }  ,(RealPoset [.0,1.]))) where z is Element of Z : verum  }  ; ::_thesis: a in  {  (((R (#) S) . (x,z)) "/\" (T . (z,w))) where z is Element of Z : verum  }
then consider z being Element of Z such that
A5: a = "\/" ( {  (((R . (x,y)) "/\" (S . (y,z))) "/\" (T . (z,w))) where y is Element of Y : verum  }  ,(RealPoset [.0,1.])) ;
 a = ((R (#) S) . (x,z)) "/\" (T . (z,w)) by A5, Lm6;
hence  a in  {  (((R (#) S) . (x,z)) "/\" (T . (z,w))) where z is Element of Z : verum  }  ; ::_thesis: verum
end;
assume  a in  {  (((R (#) S) . (x,z)) "/\" (T . (z,w))) where z is Element of Z : verum  }  ; ::_thesis: a in  {  ("\/" ( {  (((R . (x,y)) "/\" (S . (y,z))) "/\" (T . (z,w))) where y is Element of Y : verum  }  ,(RealPoset [.0,1.]))) where z is Element of Z : verum  }
then consider z being Element of Z such that
A6: a = ((R (#) S) . (x,z)) "/\" (T . (z,w)) ;
 a = "\/" ( {  (((R . (x,y)) "/\" (S . (y,z))) "/\" (T . (z,w))) where y is Element of Y : verum  }  ,(RealPoset [.0,1.])) by A6, Lm6;
hence  a in  {  ("\/" ( {  (((R . (x,y)) "/\" (S . (y,z))) "/\" (T . (z,w))) where y is Element of Y : verum  }  ,(RealPoset [.0,1.]))) where z is Element of Z : verum  }  ; ::_thesis: verum
end;
A7: for y being Element of Y
for z being Element of Z st S1[y] & S1[z] holds
H1(y,z) = H1(y,z) ;
A8: "\/" ( {  ("\/" ( {  H1(y,z) where z is Element of Z : S1[z]  }  ,(RealPoset [.0,1.]))) where y is Element of Y : S1[y]  }  ,(RealPoset [.0,1.])) = "\/" ( {  ("\/" ( {  H1(y1,z1) where y1 is Element of Y : S1[y1]  }  ,(RealPoset [.0,1.]))) where z1 is Element of Z : S1[z1]  }  ,(RealPoset [.0,1.])) from LFUZZY_0:sch_5(A7);
 for c being set holds
( c in  {  ("\/" ( {  (((R . (x,y)) "/\" (S . (y,z))) "/\" (T . (z,w))) where z is Element of Z : verum  }  ,(RealPoset [.0,1.]))) where y is Element of Y : verum  }  iff c in  {  ((R . (x,y)) "/\" ((S (#) T) . (y,w))) where y is Element of Y : verum  }  )
proof
let c be set ; ::_thesis: ( c in  {  ("\/" ( {  (((R . (x,y)) "/\" (S . (y,z))) "/\" (T . (z,w))) where z is Element of Z : verum  }  ,(RealPoset [.0,1.]))) where y is Element of Y : verum  }  iff c in  {  ((R . (x,y)) "/\" ((S (#) T) . (y,w))) where y is Element of Y : verum  }  )
hereby  ::_thesis: ( c in  {  ((R . (x,y)) "/\" ((S (#) T) . (y,w))) where y is Element of Y : verum  }  implies c in  {  ("\/" ( {  (((R . (x,y)) "/\" (S . (y,z))) "/\" (T . (z,w))) where z is Element of Z : verum  }  ,(RealPoset [.0,1.]))) where y is Element of Y : verum  }  )
assume  c in  {  ("\/" ( {  (((R . (x,y)) "/\" (S . (y,z))) "/\" (T . (z,w))) where z is Element of Z : verum  }  ,(RealPoset [.0,1.]))) where y is Element of Y : verum  }  ; ::_thesis: c in  {  ((R . (x,y)) "/\" ((S (#) T) . (y,w))) where y is Element of Y : verum  }
then consider y being Element of Y such that
A9: c = "\/" ( {  (((R . (x,y)) "/\" (S . (y,z))) "/\" (T . (z,w))) where z is Element of Z : verum  }  ,(RealPoset [.0,1.])) ;
 c = (R . (x,y)) "/\" ((S (#) T) . (y,w)) by A9, Lm7;
hence  c in  {  ((R . (x,y)) "/\" ((S (#) T) . (y,w))) where y is Element of Y : verum  }  ; ::_thesis: verum
end;
assume  c in  {  ((R . (x,y)) "/\" ((S (#) T) . (y,w))) where y is Element of Y : verum  }  ; ::_thesis: c in  {  ("\/" ( {  (((R . (x,y)) "/\" (S . (y,z))) "/\" (T . (z,w))) where z is Element of Z : verum  }  ,(RealPoset [.0,1.]))) where y is Element of Y : verum  }
then consider y being Element of Y such that
A10: c = (R . (x,y)) "/\" ((S (#) T) . (y,w)) ;
 c = "\/" ( {  (((R . (x,y)) "/\" (S . (y,z))) "/\" (T . (z,w))) where z is Element of Z : verum  }  ,(RealPoset [.0,1.])) by A10, Lm7;
hence  c in  {  ("\/" ( {  (((R . (x,y)) "/\" (S . (y,z))) "/\" (T . (z,w))) where z is Element of Z : verum  }  ,(RealPoset [.0,1.]))) where y is Element of Y : verum  }  ; ::_thesis: verum
end;
then A11:  {  ("\/" ( {  (((R . (x,y)) "/\" (S . (y,z))) "/\" (T . (z,w))) where z is Element of Z : verum  }  ,(RealPoset [.0,1.]))) where y is Element of Y : verum  }  =  {  ((R . (x,y)) "/\" ((S (#) T) . (y,w))) where y is Element of Y : verum  }  by TARSKI:1;
 ( ((R (#) S) (#) T) . (x,w) = "\/" ( {  (((R (#) S) . (x,z)) "/\" (T . (z,w))) where z is Element of Z : verum  }  ,(RealPoset [.0,1.])) & (R (#) (S (#) T)) . (x,w) = "\/" ( {  ((R . (x,y)) "/\" ((S (#) T) . (y,w))) where y is Element of Y : verum  }  ,(RealPoset [.0,1.])) ) by Th22;
hence  ((R (#) S) (#) T) . (x,w) = (R (#) (S (#) T)) . (x,w) by A4, A11, A8, TARSKI:1; ::_thesis: verum
end;
 ( dom ((R (#) S) (#) T) = [:X,W:] & dom (R (#) (S (#) T)) = [:X,W:] ) by FUNCT_2:def_1;
hence  (R (#) S) (#) T = R (#) (S (#) T) by A1, FUNCT_3:6; ::_thesis: verum
end;