:: 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;