:: LATSUM_1 semantic presentation

begin

theorem :: LATSUM_1:1
for x, y, A, B being set st x in A \/ B & y in A \/ B & not ( x in A \ B & y in A \ B ) & not ( x in B & y in B ) & not ( x in A \ B & y in B ) holds
( x in B & y in A \ B )
proof
let x, y, A, B be set ; ::_thesis: ( x in A \/ B & y in A \/ B & not ( x in A \ B & y in A \ B ) & not ( x in B & y in B ) & not ( x in A \ B & y in B ) implies ( x in B & y in A \ B ) )
assume A1: ( x in A \/ B & y in A \/ B ) ; ::_thesis: ( ( x in A \ B & y in A \ B ) or ( x in B & y in B ) or ( x in A \ B & y in B ) or ( x in B & y in A \ B ) )
 A \/ B = (A \ B) \/ B by XBOOLE_1:39;
hence  ( ( x in A \ B & y in A \ B ) or ( x in B & y in B ) or ( x in A \ B & y in B ) or ( x in B & y in A \ B ) ) by A1, XBOOLE_0:def_3; ::_thesis: verum
end;

definition
let R, S be RelStr ;
predR tolerates S means :Def1: :: LATSUM_1:def 1
 for x, y being set st x in the carrier of R /\ the carrier of S & y in the carrier of R /\ the carrier of S holds
( [x,y] in the InternalRel of R iff [x,y] in the InternalRel of S );
end;

:: deftheorem Def1 defines tolerates LATSUM_1:def_1_:_
 for R, S being RelStr holds
( R tolerates S iff for x, y being set st x in the carrier of R /\ the carrier of S & y in the carrier of R /\ the carrier of S holds
( [x,y] in the InternalRel of R iff [x,y] in the InternalRel of S ) );

begin

definition
let R, S be RelStr ;
funcR [*] S ->  strict RelStr  means :Def2: :: LATSUM_1:def 2
( the carrier of it = the carrier of R \/ the carrier of S & the InternalRel of it = ( the InternalRel of R \/ the InternalRel of S) \/ ( the InternalRel of R * the InternalRel of S) );
existence
 ex b1 being strict RelStr st
( the carrier of b1 = the carrier of R \/ the carrier of S & the InternalRel of b1 = ( the InternalRel of R \/ the InternalRel of S) \/ ( the InternalRel of R * the InternalRel of S) )
proof
set X = the carrier of R \/ the carrier of S;
 ( the carrier of R c= the carrier of R \/ the carrier of S & the carrier of S c= the carrier of R \/ the carrier of S ) by XBOOLE_1:7;
then reconsider G = the InternalRel of R * the InternalRel of S as Relation of ( the carrier of R \/ the carrier of S) by RELSET_1:7;
 ( the carrier of R c= the carrier of R \/ the carrier of S & the carrier of S c= the carrier of R \/ the carrier of S ) by XBOOLE_1:7;
then reconsider IR = the InternalRel of R, IS = the InternalRel of S as Relation of ( the carrier of R \/ the carrier of S) by RELSET_1:7;
set F = (IR \/ IS) \/ G;
reconsider F = (IR \/ IS) \/ G as Relation of ( the carrier of R \/ the carrier of S) ;
take  RelStr(# ( the carrier of R \/ the carrier of S),F #) ; ::_thesis: ( the carrier of RelStr(# ( the carrier of R \/ the carrier of S),F #) = the carrier of R \/ the carrier of S & the InternalRel of RelStr(# ( the carrier of R \/ the carrier of S),F #) = ( the InternalRel of R \/ the InternalRel of S) \/ ( the InternalRel of R * the InternalRel of S) )
thus  ( the carrier of RelStr(# ( the carrier of R \/ the carrier of S),F #) = the carrier of R \/ the carrier of S & the InternalRel of RelStr(# ( the carrier of R \/ the carrier of S),F #) = ( the InternalRel of R \/ the InternalRel of S) \/ ( the InternalRel of R * the InternalRel of S) ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict RelStr st the carrier of b1 = the carrier of R \/ the carrier of S & the InternalRel of b1 = ( the InternalRel of R \/ the InternalRel of S) \/ ( the InternalRel of R * the InternalRel of S) & the carrier of b2 = the carrier of R \/ the carrier of S & the InternalRel of b2 = ( the InternalRel of R \/ the InternalRel of S) \/ ( the InternalRel of R * the InternalRel of S) holds
b1 = b2 ;
end;

:: deftheorem Def2 defines [*] LATSUM_1:def_2_:_
 for R, S being RelStr
for b3 being strict RelStr holds
( b3 = R [*] S iff ( the carrier of b3 = the carrier of R \/ the carrier of S & the InternalRel of b3 = ( the InternalRel of R \/ the InternalRel of S) \/ ( the InternalRel of R * the InternalRel of S) ) );

registration
let R be RelStr ;
let S be non empty RelStr ;
clusterR [*] S ->  non empty strict ;
coherence
 not R [*] S is empty
proof
 the carrier of R \/ the carrier of S <> {} ;
hence  not R [*] S is empty by Def2; ::_thesis: verum
end;
end;

registration
let R be non empty RelStr ;
let S be RelStr ;
clusterR [*] S ->  non empty strict ;
coherence
 not R [*] S is empty
proof
 the carrier of R \/ the carrier of S <> {} ;
hence  not R [*] S is empty by Def2; ::_thesis: verum
end;
end;

theorem Th2: :: LATSUM_1:2
for R, S being RelStr holds
( the InternalRel of R c= the InternalRel of (R [*] S) & the InternalRel of S c= the InternalRel of (R [*] S) )
proof
let R, S be RelStr ; ::_thesis: ( the InternalRel of R c= the InternalRel of (R [*] S) & the InternalRel of S c= the InternalRel of (R [*] S) )
 ( the InternalRel of R c= the InternalRel of R \/ the InternalRel of S & the InternalRel of R \/ the InternalRel of S c= ( the InternalRel of R \/ the InternalRel of S) \/ ( the InternalRel of R * the InternalRel of S) ) by XBOOLE_1:7;
then  the InternalRel of R c= ( the InternalRel of R \/ the InternalRel of S) \/ ( the InternalRel of R * the InternalRel of S) by XBOOLE_1:1;
hence  the InternalRel of R c= the InternalRel of (R [*] S) by Def2; ::_thesis: the InternalRel of S c= the InternalRel of (R [*] S)
 ( the InternalRel of S c= the InternalRel of R \/ the InternalRel of S & the InternalRel of R \/ the InternalRel of S c= ( the InternalRel of R \/ the InternalRel of S) \/ ( the InternalRel of R * the InternalRel of S) ) by XBOOLE_1:7;
then  the InternalRel of S c= ( the InternalRel of R \/ the InternalRel of S) \/ ( the InternalRel of R * the InternalRel of S) by XBOOLE_1:1;
hence  the InternalRel of S c= the InternalRel of (R [*] S) by Def2; ::_thesis: verum
end;

theorem Th3: :: LATSUM_1:3
for R, S being RelStr st R is reflexive & S is reflexive holds
R [*] S is reflexive
proof
let R, S be RelStr ; ::_thesis: ( R is reflexive & S is reflexive implies R [*] S is reflexive )
assume  ( R is reflexive & S is reflexive ) ; ::_thesis: R [*] S is reflexive
then A1: ( the InternalRel of R is_reflexive_in the carrier of R & the InternalRel of S is_reflexive_in the carrier of S ) by ORDERS_2:def_2;
A2: ( the InternalRel of R c= the InternalRel of (R [*] S) & the InternalRel of S c= the InternalRel of (R [*] S) ) by Th2;
 the InternalRel of (R [*] S) is_reflexive_in the carrier of (R [*] S)
proof
let x be set ; :: according to RELAT_2:def_1 ::_thesis: ( not x in the carrier of (R [*] S) or [x,x] in the InternalRel of (R [*] S) )
assume  x in the carrier of (R [*] S) ; ::_thesis: [x,x] in the InternalRel of (R [*] S)
then  x in the carrier of R \/ the carrier of S by Def2;
then  ( x in the carrier of R or x in the carrier of S ) by XBOOLE_0:def_3;
then  ( [x,x] in the InternalRel of R or [x,x] in the InternalRel of S ) by A1, RELAT_2:def_1;
hence  [x,x] in the InternalRel of (R [*] S) by A2; ::_thesis: verum
end;
hence  R [*] S is reflexive by ORDERS_2:def_2; ::_thesis: verum
end;

begin

theorem Th4: :: LATSUM_1:4
for R, S being RelStr
for a, b being set st [a,b] in the InternalRel of (R [*] S) & a in the carrier of R & b in the carrier of R & R tolerates S & R is transitive holds
[a,b] in the InternalRel of R
proof
let R, S be RelStr ; ::_thesis: for a, b being set st [a,b] in the InternalRel of (R [*] S) & a in the carrier of R & b in the carrier of R & R tolerates S & R is transitive holds
[a,b] in the InternalRel of R
let a, b be set ; ::_thesis: ( [a,b] in the InternalRel of (R [*] S) & a in the carrier of R & b in the carrier of R & R tolerates S & R is transitive implies [a,b] in the InternalRel of R )
assume that
A1: [a,b] in the InternalRel of (R [*] S) and
A2: a in the carrier of R and
A3: b in the carrier of R and
A4: R tolerates S and
A5: R is transitive ; ::_thesis: [a,b] in the InternalRel of R
 [a,b] in ( the InternalRel of R \/ the InternalRel of S) \/ ( the InternalRel of R * the InternalRel of S) by A1, Def2;
then A6: ( [a,b] in the InternalRel of R \/ the InternalRel of S or [a,b] in the InternalRel of R * the InternalRel of S ) by XBOOLE_0:def_3;
assume A7: not [a,b] in the InternalRel of R ; ::_thesis: contradiction
percases ( [a,b] in the InternalRel of S or [a,b] in the InternalRel of R * the InternalRel of S ) by A7, A6, XBOOLE_0:def_3;
supposeA8: [a,b] in the InternalRel of S ; ::_thesis: contradiction
then  b in the carrier of S by ZFMISC_1:87;
then A9: b in the carrier of R /\ the carrier of S by A3, XBOOLE_0:def_4;
 a in the carrier of S by A8, ZFMISC_1:87;
then  a in the carrier of R /\ the carrier of S by A2, XBOOLE_0:def_4;
hence  contradiction by A4, A7, A8, A9, Def1; ::_thesis: verum
end;
supposeA10: [a,b] in the InternalRel of R * the InternalRel of S ; ::_thesis: contradiction
then  b in the carrier of S by ZFMISC_1:87;
then A11: b in the carrier of R /\ the carrier of S by A3, XBOOLE_0:def_4;
A12: the InternalRel of R is_transitive_in the carrier of R by A5, ORDERS_2:def_3;
consider z being set  such that
A13: [a,z] in the InternalRel of R and
A14: [z,b] in the InternalRel of S by A10, RELAT_1:def_8;
A15: z in the carrier of R by A13, ZFMISC_1:87;
 z in the carrier of S by A14, ZFMISC_1:87;
then  z in the carrier of R /\ the carrier of S by A15, XBOOLE_0:def_4;
then  [z,b] in the InternalRel of R by A4, A11, A14, Def1;
hence  contradiction by A2, A3, A7, A13, A15, A12, RELAT_2:def_8; ::_thesis: verum
end;
end;
end;

theorem Th5: :: LATSUM_1:5
for R, S being RelStr
for a, b being set st [a,b] in the InternalRel of (R [*] S) & a in the carrier of S & b in the carrier of S & R tolerates S & S is transitive holds
[a,b] in the InternalRel of S
proof
let R, S be RelStr ; ::_thesis: for a, b being set st [a,b] in the InternalRel of (R [*] S) & a in the carrier of S & b in the carrier of S & R tolerates S & S is transitive holds
[a,b] in the InternalRel of S
let a, b be set ; ::_thesis: ( [a,b] in the InternalRel of (R [*] S) & a in the carrier of S & b in the carrier of S & R tolerates S & S is transitive implies [a,b] in the InternalRel of S )
assume that
A1: [a,b] in the InternalRel of (R [*] S) and
A2: a in the carrier of S and
A3: b in the carrier of S and
A4: R tolerates S and
A5: S is transitive ; ::_thesis: [a,b] in the InternalRel of S
 [a,b] in ( the InternalRel of R \/ the InternalRel of S) \/ ( the InternalRel of R * the InternalRel of S) by A1, Def2;
then A6: ( [a,b] in the InternalRel of R \/ the InternalRel of S or [a,b] in the InternalRel of R * the InternalRel of S ) by XBOOLE_0:def_3;
assume A7: not [a,b] in the InternalRel of S ; ::_thesis: contradiction
percases ( [a,b] in the InternalRel of R or [a,b] in the InternalRel of R * the InternalRel of S ) by A7, A6, XBOOLE_0:def_3;
supposeA8: [a,b] in the InternalRel of R ; ::_thesis: contradiction
then  b in the carrier of R by ZFMISC_1:87;
then A9: b in the carrier of R /\ the carrier of S by A3, XBOOLE_0:def_4;
 a in the carrier of R by A8, ZFMISC_1:87;
then  a in the carrier of R /\ the carrier of S by A2, XBOOLE_0:def_4;
hence  contradiction by A4, A7, A8, A9, Def1; ::_thesis: verum
end;
supposeA10: [a,b] in the InternalRel of R * the InternalRel of S ; ::_thesis: contradiction
then  a in the carrier of R by ZFMISC_1:87;
then A11: a in the carrier of R /\ the carrier of S by A2, XBOOLE_0:def_4;
A12: the InternalRel of S is_transitive_in the carrier of S by A5, ORDERS_2:def_3;
consider z being set  such that
A13: [a,z] in the InternalRel of R and
A14: [z,b] in the InternalRel of S by A10, RELAT_1:def_8;
A15: z in the carrier of S by A14, ZFMISC_1:87;
 z in the carrier of R by A13, ZFMISC_1:87;
then  z in the carrier of R /\ the carrier of S by A15, XBOOLE_0:def_4;
then  [a,z] in the InternalRel of S by A4, A11, A13, Def1;
hence  contradiction by A2, A3, A7, A14, A15, A12, RELAT_2:def_8; ::_thesis: verum
end;
end;
end;

theorem Th6: :: LATSUM_1:6
for R, S being RelStr
for a, b being set holds
( ( [a,b] in the InternalRel of R implies [a,b] in the InternalRel of (R [*] S) ) & ( [a,b] in the InternalRel of S implies [a,b] in the InternalRel of (R [*] S) ) )
proof
let R, S be RelStr ; ::_thesis: for a, b being set holds
( ( [a,b] in the InternalRel of R implies [a,b] in the InternalRel of (R [*] S) ) & ( [a,b] in the InternalRel of S implies [a,b] in the InternalRel of (R [*] S) ) )
let a, b be set ; ::_thesis: ( ( [a,b] in the InternalRel of R implies [a,b] in the InternalRel of (R [*] S) ) & ( [a,b] in the InternalRel of S implies [a,b] in the InternalRel of (R [*] S) ) )
thus  ( [a,b] in the InternalRel of R implies [a,b] in the InternalRel of (R [*] S) ) ::_thesis: ( [a,b] in the InternalRel of S implies [a,b] in the InternalRel of (R [*] S) )
proof
assume  [a,b] in the InternalRel of R ; ::_thesis: [a,b] in the InternalRel of (R [*] S)
then  [a,b] in the InternalRel of R \/ the InternalRel of S by XBOOLE_0:def_3;
then  [a,b] in ( the InternalRel of R \/ the InternalRel of S) \/ ( the InternalRel of R * the InternalRel of S) by XBOOLE_0:def_3;
hence  [a,b] in the InternalRel of (R [*] S) by Def2; ::_thesis: verum
end;
assume  [a,b] in the InternalRel of S ; ::_thesis: [a,b] in the InternalRel of (R [*] S)
then  [a,b] in the InternalRel of R \/ the InternalRel of S by XBOOLE_0:def_3;
then  [a,b] in ( the InternalRel of R \/ the InternalRel of S) \/ ( the InternalRel of R * the InternalRel of S) by XBOOLE_0:def_3;
hence  [a,b] in the InternalRel of (R [*] S) by Def2; ::_thesis: verum
end;

theorem :: LATSUM_1:7
for R, S being non empty RelStr
for x being Element of (R [*] S) holds
( x in the carrier of R or x in the carrier of S \ the carrier of R )
proof
let R, S be non empty RelStr ; ::_thesis: for x being Element of (R [*] S) holds
( x in the carrier of R or x in the carrier of S \ the carrier of R )
let x be Element of (R [*] S); ::_thesis: ( x in the carrier of R or x in the carrier of S \ the carrier of R )
 x in the carrier of (R [*] S) ;
then  x in the carrier of S \/ the carrier of R by Def2;
then  x in the carrier of R \/ ( the carrier of S \ the carrier of R) by XBOOLE_1:39;
hence  ( x in the carrier of R or x in the carrier of S \ the carrier of R ) by XBOOLE_0:def_3; ::_thesis: verum
end;

theorem Th8: :: LATSUM_1:8
for R, S being non empty RelStr
for x, y being Element of R
for a, b being Element of (R [*] S) st x = a & y = b & R tolerates S & R is transitive holds
( x <= y iff a <= b )
proof
let R, S be non empty RelStr ; ::_thesis: for x, y being Element of R
for a, b being Element of (R [*] S) st x = a & y = b & R tolerates S & R is transitive holds
( x <= y iff a <= b )
let x, y be Element of R; ::_thesis: for a, b being Element of (R [*] S) st x = a & y = b & R tolerates S & R is transitive holds
( x <= y iff a <= b )
let a, b be Element of (R [*] S); ::_thesis: ( x = a & y = b & R tolerates S & R is transitive implies ( x <= y iff a <= b ) )
assume A1: ( x = a & y = b ) ; ::_thesis: ( not R tolerates S or not R is transitive or ( x <= y iff a <= b ) )
assume A2: ( R tolerates S & R is transitive ) ; ::_thesis: ( x <= y iff a <= b )
hereby  ::_thesis: ( a <= b implies x <= y )
assume  x <= y ; ::_thesis: a <= b
then  [x,y] in the InternalRel of R by ORDERS_2:def_5;
then  [a,b] in the InternalRel of (R [*] S) by A1, Th6;
hence  a <= b by ORDERS_2:def_5; ::_thesis: verum
end;
assume  a <= b ; ::_thesis: x <= y
then  [a,b] in the InternalRel of (R [*] S) by ORDERS_2:def_5;
then  [x,y] in the InternalRel of R by A1, A2, Th4;
hence  x <= y by ORDERS_2:def_5; ::_thesis: verum
end;

theorem Th9: :: LATSUM_1:9
for R, S being non empty RelStr
for a, b being Element of (R [*] S)
for c, d being Element of S st a = c & b = d & R tolerates S & S is transitive holds
( a <= b iff c <= d )
proof
let R, S be non empty RelStr ; ::_thesis: for a, b being Element of (R [*] S)
for c, d being Element of S st a = c & b = d & R tolerates S & S is transitive holds
( a <= b iff c <= d )
let a, b be Element of (R [*] S); ::_thesis: for c, d being Element of S st a = c & b = d & R tolerates S & S is transitive holds
( a <= b iff c <= d )
let c, d be Element of S; ::_thesis: ( a = c & b = d & R tolerates S & S is transitive implies ( a <= b iff c <= d ) )
assume that
A1: ( a = c & b = d ) and
A2: ( R tolerates S & S is transitive ) ; ::_thesis: ( a <= b iff c <= d )
hereby  ::_thesis: ( c <= d implies a <= b )
assume  a <= b ; ::_thesis: c <= d
then  [a,b] in the InternalRel of (R [*] S) by ORDERS_2:def_5;
then  [c,d] in the InternalRel of S by A1, A2, Th5;
hence  c <= d by ORDERS_2:def_5; ::_thesis: verum
end;
assume  c <= d ; ::_thesis: a <= b
then  [c,d] in the InternalRel of S by ORDERS_2:def_5;
then  [a,b] in the InternalRel of (R [*] S) by A1, Th6;
hence  a <= b by ORDERS_2:def_5; ::_thesis: verum
end;

theorem Th10: :: LATSUM_1:10
for R, S being non empty reflexive transitive antisymmetric with_suprema RelStr
for x being set st x in the carrier of R holds
x is Element of (R [*] S)
proof
let R, S be non empty reflexive transitive antisymmetric with_suprema RelStr ; ::_thesis: for x being set st x in the carrier of R holds
x is Element of (R [*] S)
let x be set ; ::_thesis: ( x in the carrier of R implies x is Element of (R [*] S) )
assume  x in the carrier of R ; ::_thesis: x is Element of (R [*] S)
then  x in the carrier of R \/ the carrier of S by XBOOLE_0:def_3;
hence  x is Element of (R [*] S) by Def2; ::_thesis: verum
end;

theorem :: LATSUM_1:11
for R, S being non empty reflexive transitive antisymmetric with_suprema RelStr
for x being set st x in the carrier of S holds
x is Element of (R [*] S)
proof
let R, S be non empty reflexive transitive antisymmetric with_suprema RelStr ; ::_thesis: for x being set st x in the carrier of S holds
x is Element of (R [*] S)
let x be set ; ::_thesis: ( x in the carrier of S implies x is Element of (R [*] S) )
assume  x in the carrier of S ; ::_thesis: x is Element of (R [*] S)
then  x in the carrier of R \/ the carrier of S by XBOOLE_0:def_3;
hence  x is Element of (R [*] S) by Def2; ::_thesis: verum
end;

theorem Th12: :: LATSUM_1:12
for R, S being non empty RelStr
for x being set st x in the carrier of R /\ the carrier of S holds
x is Element of R
proof
let R, S be non empty RelStr ; ::_thesis: for x being set st x in the carrier of R /\ the carrier of S holds
x is Element of R
let x be set ; ::_thesis: ( x in the carrier of R /\ the carrier of S implies x is Element of R )
assume A1: x in the carrier of R /\ the carrier of S ; ::_thesis: x is Element of R
 the carrier of R /\ the carrier of S c= the carrier of R by XBOOLE_1:17;
hence  x is Element of R by A1; ::_thesis: verum
end;

theorem Th13: :: LATSUM_1:13
for R, S being non empty RelStr
for x being set st x in the carrier of R /\ the carrier of S holds
x is Element of S
proof
let R, S be non empty RelStr ; ::_thesis: for x being set st x in the carrier of R /\ the carrier of S holds
x is Element of S
let x be set ; ::_thesis: ( x in the carrier of R /\ the carrier of S implies x is Element of S )
assume A1: x in the carrier of R /\ the carrier of S ; ::_thesis: x is Element of S
 the carrier of R /\ the carrier of S c= the carrier of S by XBOOLE_1:17;
hence  x is Element of S by A1; ::_thesis: verum
end;

theorem :: LATSUM_1:14
for R, S being non empty reflexive transitive antisymmetric with_suprema RelStr
for x, y being Element of (R [*] S) st x in the carrier of R & y in the carrier of S & R tolerates S holds
( x <= y iff ex a being Element of (R [*] S) st
( a in the carrier of R /\ the carrier of S & x <= a & a <= y ) )
proof
let R, S be non empty reflexive transitive antisymmetric with_suprema RelStr ; ::_thesis: for x, y being Element of (R [*] S) st x in the carrier of R & y in the carrier of S & R tolerates S holds
( x <= y iff ex a being Element of (R [*] S) st
( a in the carrier of R /\ the carrier of S & x <= a & a <= y ) )
let x, y be Element of (R [*] S); ::_thesis: ( x in the carrier of R & y in the carrier of S & R tolerates S implies ( x <= y iff ex a being Element of (R [*] S) st
( a in the carrier of R /\ the carrier of S & x <= a & a <= y ) ) )
assume that
A1: x in the carrier of R and
A2: y in the carrier of S and
A3: R tolerates S ; ::_thesis: ( x <= y iff ex a being Element of (R [*] S) st
( a in the carrier of R /\ the carrier of S & x <= a & a <= y ) )
percases ( [x,y] in the InternalRel of R or [x,y] in the InternalRel of S or ( not [x,y] in the InternalRel of R & not [x,y] in the InternalRel of S ) ) ;
supposeA4: [x,y] in the InternalRel of R ; ::_thesis: ( x <= y iff ex a being Element of (R [*] S) st
( a in the carrier of R /\ the carrier of S & x <= a & a <= y ) )
hereby  ::_thesis: ( ex a being Element of (R [*] S) st
( a in the carrier of R /\ the carrier of S & x <= a & a <= y ) implies x <= y )
assume A5: x <= y ; ::_thesis: ex a being Element of (R [*] S) st
( a in the carrier of R /\ the carrier of S & x <= a & a <= y )
take a = y; ::_thesis: ( a in the carrier of R /\ the carrier of S & x <= a & a <= y )
 y in the carrier of R by A4, ZFMISC_1:87;
hence  a in the carrier of R /\ the carrier of S by A2, XBOOLE_0:def_4; ::_thesis: ( x <= a & a <= y )
 R [*] S is reflexive by Th3;
hence  ( x <= a & a <= y ) by A5, ORDERS_2:1; ::_thesis: verum
end;
 [x,y] in the InternalRel of (R [*] S) by A4, Th6;
hence  ( ex a being Element of (R [*] S) st
( a in the carrier of R /\ the carrier of S & x <= a & a <= y ) implies x <= y ) by ORDERS_2:def_5; ::_thesis: verum
end;
supposeA6: [x,y] in the InternalRel of S ; ::_thesis: ( x <= y iff ex a being Element of (R [*] S) st
( a in the carrier of R /\ the carrier of S & x <= a & a <= y ) )
hereby  ::_thesis: ( ex a being Element of (R [*] S) st
( a in the carrier of R /\ the carrier of S & x <= a & a <= y ) implies x <= y )
assume A7: x <= y ; ::_thesis: ex a being Element of (R [*] S) st
( a in the carrier of R /\ the carrier of S & x <= a & a <= y )
take a = x; ::_thesis: ( a in the carrier of R /\ the carrier of S & x <= a & a <= y )
 x in the carrier of S by A6, ZFMISC_1:87;
hence  a in the carrier of R /\ the carrier of S by A1, XBOOLE_0:def_4; ::_thesis: ( x <= a & a <= y )
 R [*] S is reflexive by Th3;
hence  ( x <= a & a <= y ) by A7, ORDERS_2:1; ::_thesis: verum
end;
 [x,y] in the InternalRel of (R [*] S) by A6, Th6;
hence  ( ex a being Element of (R [*] S) st
( a in the carrier of R /\ the carrier of S & x <= a & a <= y ) implies x <= y ) by ORDERS_2:def_5; ::_thesis: verum
end;
supposeA8: ( not [x,y] in the InternalRel of R & not [x,y] in the InternalRel of S ) ; ::_thesis: ( x <= y iff ex a being Element of (R [*] S) st
( a in the carrier of R /\ the carrier of S & x <= a & a <= y ) )
hereby  ::_thesis: ( ex a being Element of (R [*] S) st
( a in the carrier of R /\ the carrier of S & x <= a & a <= y ) implies x <= y )
assume  x <= y ; ::_thesis: ex z being Element of (R [*] S) st
( z in the carrier of R /\ the carrier of S & x <= z & z <= y )
then  [x,y] in the InternalRel of (R [*] S) by ORDERS_2:def_5;
then  [x,y] in ( the InternalRel of R \/ the InternalRel of S) \/ ( the InternalRel of R * the InternalRel of S) by Def2;
then  ( [x,y] in the InternalRel of R \/ the InternalRel of S or [x,y] in the InternalRel of R * the InternalRel of S ) by XBOOLE_0:def_3;
then consider z being set  such that
A9: [x,z] in the InternalRel of R and
A10: [z,y] in the InternalRel of S by A8, RELAT_1:def_8, XBOOLE_0:def_3;
A11: z in the carrier of R by A9, ZFMISC_1:87;
A12: z in the carrier of S by A10, ZFMISC_1:87;
then  z in the carrier of R \/ the carrier of S by XBOOLE_0:def_3;
then reconsider z = z as Element of (R [*] S) by Def2;
take z = z; ::_thesis: ( z in the carrier of R /\ the carrier of S & x <= z & z <= y )
thus  z in the carrier of R /\ the carrier of S by A11, A12, XBOOLE_0:def_4; ::_thesis: ( x <= z & z <= y )
 [x,z] in the InternalRel of (R [*] S) by A9, Th6;
hence  x <= z by ORDERS_2:def_5; ::_thesis: z <= y
 [z,y] in the InternalRel of (R [*] S) by A10, Th6;
hence  z <= y by ORDERS_2:def_5; ::_thesis: verum
end;
given a being Element of (R [*] S) such that A13: a in the carrier of R /\ the carrier of S and
A14: x <= a and
A15: a <= y ; ::_thesis: x <= y
reconsider y9 = y, a1 = a as Element of S by A2, A13, Th13;
 a1 <= y9 by A3, A15, Th9;
then A16: [a,y] in the InternalRel of S by ORDERS_2:def_5;
reconsider x9 = x, a9 = a as Element of R by A1, A13, Th12;
 x9 <= a9 by A3, A14, Th8;
then  [x,a] in the InternalRel of R by ORDERS_2:def_5;
then  [x,y] in the InternalRel of R * the InternalRel of S by A16, RELAT_1:def_8;
then  [x,y] in ( the InternalRel of R \/ the InternalRel of S) \/ ( the InternalRel of R * the InternalRel of S) by XBOOLE_0:def_3;
then  [x,y] in the InternalRel of (R [*] S) by Def2;
hence  x <= y by ORDERS_2:def_5; ::_thesis: verum
end;
end;
end;

theorem Th15: :: LATSUM_1:15
for R, S being non empty RelStr
for a, b being Element of R
for c, d being Element of S st a = c & b = d & R tolerates S & R is transitive & S is transitive holds
( a <= b iff c <= d )
proof
let R, S be non empty RelStr ; ::_thesis: for a, b being Element of R
for c, d being Element of S st a = c & b = d & R tolerates S & R is transitive & S is transitive holds
( a <= b iff c <= d )
let a, b be Element of R; ::_thesis: for c, d being Element of S st a = c & b = d & R tolerates S & R is transitive & S is transitive holds
( a <= b iff c <= d )
let c, d be Element of S; ::_thesis: ( a = c & b = d & R tolerates S & R is transitive & S is transitive implies ( a <= b iff c <= d ) )
assume that
A1: ( a = c & b = d ) and
A2: R tolerates S and
A3: R is transitive and
A4: S is transitive ; ::_thesis: ( a <= b iff c <= d )
 ( a in the carrier of R \/ the carrier of S & b in the carrier of R \/ the carrier of S ) by XBOOLE_0:def_3;
then reconsider a9 = a, b9 = b as Element of (R [*] S) by Def2;
hereby  ::_thesis: ( c <= d implies a <= b )
assume  a <= b ; ::_thesis: c <= d
then  a9 <= b9 by A2, A3, Th8;
hence  c <= d by A1, A2, A4, Th9; ::_thesis: verum
end;
assume  c <= d ; ::_thesis: a <= b
then  a9 <= b9 by A1, A2, A4, Th9;
hence  a <= b by A2, A3, Th8; ::_thesis: verum
end;

theorem Th16: :: LATSUM_1:16
for R being non empty reflexive transitive antisymmetric with_suprema RelStr
for D being directed lower Subset of R
for x, y being Element of R st x in D & y in D holds
x "\/" y in D
proof
let R be non empty reflexive transitive antisymmetric with_suprema RelStr ; ::_thesis: for D being directed lower Subset of R
for x, y being Element of R st x in D & y in D holds
x "\/" y in D
let D be directed lower Subset of R; ::_thesis: for x, y being Element of R st x in D & y in D holds
x "\/" y in D
let x, y be Element of R; ::_thesis: ( x in D & y in D implies x "\/" y in D )
assume  ( x in D & y in D ) ; ::_thesis: x "\/" y in D
then consider z being Element of R such that
A1: z in D and
A2: ( x <= z & y <= z ) by WAYBEL_0:def_1;
 x "\/" y <= z by A2, YELLOW_0:22;
hence  x "\/" y in D by A1, WAYBEL_0:def_19; ::_thesis: verum
end;

theorem Th17: :: LATSUM_1:17
for R, S being RelStr
for a, b being set st the carrier of R /\ the carrier of S is upper Subset of R & [a,b] in the InternalRel of (R [*] S) & a in the carrier of S holds
b in the carrier of S
proof
let R, S be RelStr ; ::_thesis: for a, b being set st the carrier of R /\ the carrier of S is upper Subset of R & [a,b] in the InternalRel of (R [*] S) & a in the carrier of S holds
b in the carrier of S
let a, b be set ; ::_thesis: ( the carrier of R /\ the carrier of S is upper Subset of R & [a,b] in the InternalRel of (R [*] S) & a in the carrier of S implies b in the carrier of S )
set X = the carrier of R /\ the carrier of S;
reconsider X = the carrier of R /\ the carrier of S as Subset of R by XBOOLE_1:17;
assume that
A1: the carrier of R /\ the carrier of S is upper Subset of R and
A2: [a,b] in the InternalRel of (R [*] S) and
A3: a in the carrier of S ; ::_thesis: b in the carrier of S
 [a,b] in ( the InternalRel of R \/ the InternalRel of S) \/ ( the InternalRel of R * the InternalRel of S) by A2, Def2;
then A4: ( [a,b] in the InternalRel of R \/ the InternalRel of S or [a,b] in the InternalRel of R * the InternalRel of S ) by XBOOLE_0:def_3;
assume A5: not b in the carrier of S ; ::_thesis: contradiction
percases ( [a,b] in the InternalRel of R or [a,b] in the InternalRel of S or [a,b] in the InternalRel of R * the InternalRel of S ) by A4, XBOOLE_0:def_3;
supposeA6: [a,b] in the InternalRel of R ; ::_thesis: contradiction
then reconsider a9 = a, b9 = b as Element of R by ZFMISC_1:87;
 a in the carrier of R by A6, ZFMISC_1:87;
then A7: a in the carrier of R /\ the carrier of S by A3, XBOOLE_0:def_4;
 a9 <= b9 by A6, ORDERS_2:def_5;
then  ( X c= the carrier of S & b in X ) by A1, A7, WAYBEL_0:def_20, XBOOLE_1:17;
hence  contradiction by A5; ::_thesis: verum
end;
suppose [a,b] in the InternalRel of S ; ::_thesis: contradiction
hence  contradiction by A5, ZFMISC_1:87; ::_thesis: verum
end;
suppose [a,b] in the InternalRel of R * the InternalRel of S ; ::_thesis: contradiction
hence  contradiction by A5, ZFMISC_1:87; ::_thesis: verum
end;
end;
end;

theorem Th18: :: LATSUM_1:18
for R, S being RelStr
for a, b being Element of (R [*] S) st the carrier of R /\ the carrier of S is upper Subset of R & a <= b & a in the carrier of S holds
b in the carrier of S
proof
let R, S be RelStr ; ::_thesis: for a, b being Element of (R [*] S) st the carrier of R /\ the carrier of S is upper Subset of R & a <= b & a in the carrier of S holds
b in the carrier of S
let a, b be Element of (R [*] S); ::_thesis: ( the carrier of R /\ the carrier of S is upper Subset of R & a <= b & a in the carrier of S implies b in the carrier of S )
assume that
A1: the carrier of R /\ the carrier of S is upper Subset of R and
A2: a <= b and
A3: a in the carrier of S ; ::_thesis: b in the carrier of S
 [a,b] in the InternalRel of (R [*] S) by A2, ORDERS_2:def_5;
hence  b in the carrier of S by A1, A3, Th17; ::_thesis: verum
end;

theorem :: LATSUM_1:19
for R, S being non empty reflexive transitive antisymmetric with_suprema RelStr
for x, y being Element of R
for a, b being Element of S st the carrier of R /\ the carrier of S is directed lower Subset of S & the carrier of R /\ the carrier of S is upper Subset of R & R tolerates S & x = a & y = b holds
x "\/" y = a "\/" b
proof
let R, S be non empty reflexive transitive antisymmetric with_suprema RelStr ; ::_thesis: for x, y being Element of R
for a, b being Element of S st the carrier of R /\ the carrier of S is directed lower Subset of S & the carrier of R /\ the carrier of S is upper Subset of R & R tolerates S & x = a & y = b holds
x "\/" y = a "\/" b
let x, y be Element of R; ::_thesis: for a, b being Element of S st the carrier of R /\ the carrier of S is directed lower Subset of S & the carrier of R /\ the carrier of S is upper Subset of R & R tolerates S & x = a & y = b holds
x "\/" y = a "\/" b
let a, b be Element of S; ::_thesis: ( the carrier of R /\ the carrier of S is directed lower Subset of S & the carrier of R /\ the carrier of S is upper Subset of R & R tolerates S & x = a & y = b implies x "\/" y = a "\/" b )
assume that
A1: the carrier of R /\ the carrier of S is directed lower Subset of S and
A2: the carrier of R /\ the carrier of S is upper Subset of R and
A3: R tolerates S and
A4: x = a and
A5: y = b ; ::_thesis: x "\/" y = a "\/" b
 ( a in the carrier of R /\ the carrier of S & b in the carrier of R /\ the carrier of S ) by A4, A5, XBOOLE_0:def_4;
then reconsider xy = a "\/" b as Element of R by A1, Th13, Th16;
 a "\/" b >= b by YELLOW_0:22;
then A6: xy >= y by A3, A5, Th15;
A7: for d being Element of R st d >= x & d >= y holds
xy <= d
proof
let d be Element of R; ::_thesis: ( d >= x & d >= y implies xy <= d )
reconsider X = x, D = d as Element of (R [*] S) by Th10;
assume that
A8: d >= x and
A9: d >= y ; ::_thesis: xy <= d
 X <= D by A3, A8, Th8;
then reconsider dd = d as Element of S by A2, A4, Th18;
 ( dd >= a & b <= dd ) by A3, A4, A5, A8, A9, Th15;
then  a "\/" b <= dd by YELLOW_5:9;
hence  xy <= d by A3, Th15; ::_thesis: verum
end;
 a "\/" b >= a by YELLOW_0:22;
then  xy >= x by A3, A4, Th15;
hence  x "\/" y = a "\/" b by A6, A7, YELLOW_0:22; ::_thesis: verum
end;

theorem :: LATSUM_1:20
for R, S being non empty reflexive transitive antisymmetric with_suprema lower-bounded RelStr st the carrier of R /\ the carrier of S is non empty directed lower Subset of S holds
Bottom S in the carrier of R
proof
let R, S be non empty reflexive transitive antisymmetric with_suprema lower-bounded RelStr ; ::_thesis: ( the carrier of R /\ the carrier of S is non empty directed lower Subset of S implies Bottom S in the carrier of R )
assume A1: the carrier of R /\ the carrier of S is non empty directed lower Subset of S ; ::_thesis: Bottom S in the carrier of R
then consider x being set  such that
A2: x in the carrier of R /\ the carrier of S by XBOOLE_0:def_1;
reconsider x = x as Element of S by A2, Th13;
 Bottom S <= x by YELLOW_0:44;
then  Bottom S in the carrier of R /\ the carrier of S by A1, A2, WAYBEL_0:def_19;
hence  Bottom S in the carrier of R by XBOOLE_0:def_4; ::_thesis: verum
end;

theorem Th21: :: LATSUM_1:21
for R, S being RelStr
for a, b being set st the carrier of R /\ the carrier of S is lower Subset of S & [a,b] in the InternalRel of (R [*] S) & b in the carrier of R holds
a in the carrier of R
proof
let R, S be RelStr ; ::_thesis: for a, b being set st the carrier of R /\ the carrier of S is lower Subset of S & [a,b] in the InternalRel of (R [*] S) & b in the carrier of R holds
a in the carrier of R
let a, b be set ; ::_thesis: ( the carrier of R /\ the carrier of S is lower Subset of S & [a,b] in the InternalRel of (R [*] S) & b in the carrier of R implies a in the carrier of R )
set X = the carrier of R /\ the carrier of S;
reconsider X = the carrier of R /\ the carrier of S as Subset of R by XBOOLE_1:17;
assume that
A1: the carrier of R /\ the carrier of S is lower Subset of S and
A2: [a,b] in the InternalRel of (R [*] S) and
A3: b in the carrier of R ; ::_thesis: a in the carrier of R
 [a,b] in ( the InternalRel of R \/ the InternalRel of S) \/ ( the InternalRel of R * the InternalRel of S) by A2, Def2;
then A4: ( [a,b] in the InternalRel of R \/ the InternalRel of S or [a,b] in the InternalRel of R * the InternalRel of S ) by XBOOLE_0:def_3;
assume A5: not a in the carrier of R ; ::_thesis: contradiction
percases ( [a,b] in the InternalRel of S or [a,b] in the InternalRel of R or [a,b] in the InternalRel of R * the InternalRel of S ) by A4, XBOOLE_0:def_3;
supposeA6: [a,b] in the InternalRel of S ; ::_thesis: contradiction
then reconsider a9 = a, b9 = b as Element of S by ZFMISC_1:87;
 b in the carrier of S by A6, ZFMISC_1:87;
then A7: b in the carrier of R /\ the carrier of S by A3, XBOOLE_0:def_4;
 a9 <= b9 by A6, ORDERS_2:def_5;
then  a in X by A1, A7, WAYBEL_0:def_19;
hence  contradiction by A5; ::_thesis: verum
end;
suppose [a,b] in the InternalRel of R ; ::_thesis: contradiction
hence  contradiction by A5, ZFMISC_1:87; ::_thesis: verum
end;
suppose [a,b] in the InternalRel of R * the InternalRel of S ; ::_thesis: contradiction
hence  contradiction by A5, ZFMISC_1:87; ::_thesis: verum
end;
end;
end;

theorem :: LATSUM_1:22
for x, y being set
for R, S being RelStr st [x,y] in the InternalRel of (R [*] S) & the carrier of R /\ the carrier of S is upper Subset of R & not ( x in the carrier of R & y in the carrier of R ) & not ( x in the carrier of S & y in the carrier of S ) holds
( x in the carrier of R \ the carrier of S & y in the carrier of S \ the carrier of R )
proof
let x, y be set ; ::_thesis: for R, S being RelStr st [x,y] in the InternalRel of (R [*] S) & the carrier of R /\ the carrier of S is upper Subset of R & not ( x in the carrier of R & y in the carrier of R ) & not ( x in the carrier of S & y in the carrier of S ) holds
( x in the carrier of R \ the carrier of S & y in the carrier of S \ the carrier of R )
let R, S be RelStr ; ::_thesis: ( [x,y] in the InternalRel of (R [*] S) & the carrier of R /\ the carrier of S is upper Subset of R & not ( x in the carrier of R & y in the carrier of R ) & not ( x in the carrier of S & y in the carrier of S ) implies ( x in the carrier of R \ the carrier of S & y in the carrier of S \ the carrier of R ) )
assume that
A1: [x,y] in the InternalRel of (R [*] S) and
A2: the carrier of R /\ the carrier of S is upper Subset of R ; ::_thesis: ( ( x in the carrier of R & y in the carrier of R ) or ( x in the carrier of S & y in the carrier of S ) or ( x in the carrier of R \ the carrier of S & y in the carrier of S \ the carrier of R ) )
 x in the carrier of (R [*] S) by A1, ZFMISC_1:87;
then A3: x in the carrier of R \/ the carrier of S by Def2;
 y in the carrier of (R [*] S) by A1, ZFMISC_1:87;
then A4: y in the carrier of R \/ the carrier of S by Def2;
percases ( ( x in the carrier of R & y in the carrier of R ) or ( x in the carrier of S & y in the carrier of S ) or ( x in the carrier of R & y in the carrier of S ) or ( x in the carrier of S & y in the carrier of R ) ) by A3, A4, XBOOLE_0:def_3;
suppose ( x in the carrier of R & y in the carrier of R ) ; ::_thesis: ( ( x in the carrier of R & y in the carrier of R ) or ( x in the carrier of S & y in the carrier of S ) or ( x in the carrier of R \ the carrier of S & y in the carrier of S \ the carrier of R ) )
hence  ( ( x in the carrier of R & y in the carrier of R ) or ( x in the carrier of S & y in the carrier of S ) or ( x in the carrier of R \ the carrier of S & y in the carrier of S \ the carrier of R ) ) ; ::_thesis: verum
end;
suppose ( x in the carrier of S & y in the carrier of S ) ; ::_thesis: ( ( x in the carrier of R & y in the carrier of R ) or ( x in the carrier of S & y in the carrier of S ) or ( x in the carrier of R \ the carrier of S & y in the carrier of S \ the carrier of R ) )
hence  ( ( x in the carrier of R & y in the carrier of R ) or ( x in the carrier of S & y in the carrier of S ) or ( x in the carrier of R \ the carrier of S & y in the carrier of S \ the carrier of R ) ) ; ::_thesis: verum
end;
suppose ( x in the carrier of R & y in the carrier of S ) ; ::_thesis: ( ( x in the carrier of R & y in the carrier of R ) or ( x in the carrier of S & y in the carrier of S ) or ( x in the carrier of R \ the carrier of S & y in the carrier of S \ the carrier of R ) )
hence  ( ( x in the carrier of R & y in the carrier of R ) or ( x in the carrier of S & y in the carrier of S ) or ( x in the carrier of R \ the carrier of S & y in the carrier of S \ the carrier of R ) ) by XBOOLE_0:def_5; ::_thesis: verum
end;
suppose ( x in the carrier of S & y in the carrier of R ) ; ::_thesis: ( ( x in the carrier of R & y in the carrier of R ) or ( x in the carrier of S & y in the carrier of S ) or ( x in the carrier of R \ the carrier of S & y in the carrier of S \ the carrier of R ) )
hence  ( ( x in the carrier of R & y in the carrier of R ) or ( x in the carrier of S & y in the carrier of S ) or ( x in the carrier of R \ the carrier of S & y in the carrier of S \ the carrier of R ) ) by A1, A2, Th17; ::_thesis: verum
end;
end;
end;

theorem :: LATSUM_1:23
for R, S being RelStr
for a, b being Element of (R [*] S) st the carrier of R /\ the carrier of S is lower Subset of S & a <= b & b in the carrier of R holds
a in the carrier of R
proof
let R, S be RelStr ; ::_thesis: for a, b being Element of (R [*] S) st the carrier of R /\ the carrier of S is lower Subset of S & a <= b & b in the carrier of R holds
a in the carrier of R
let a, b be Element of (R [*] S); ::_thesis: ( the carrier of R /\ the carrier of S is lower Subset of S & a <= b & b in the carrier of R implies a in the carrier of R )
assume that
A1: the carrier of R /\ the carrier of S is lower Subset of S and
A2: a <= b and
A3: b in the carrier of R ; ::_thesis: a in the carrier of R
 [a,b] in the InternalRel of (R [*] S) by A2, ORDERS_2:def_5;
hence  a in the carrier of R by A1, A3, Th21; ::_thesis: verum
end;

theorem :: LATSUM_1:24
for R, S being RelStr st R tolerates S & the carrier of R /\ the carrier of S is upper Subset of R & the carrier of R /\ the carrier of S is lower Subset of S & R is transitive & R is antisymmetric & S is transitive & S is antisymmetric holds
R [*] S is antisymmetric
proof
let R, S be RelStr ; ::_thesis: ( R tolerates S & the carrier of R /\ the carrier of S is upper Subset of R & the carrier of R /\ the carrier of S is lower Subset of S & R is transitive & R is antisymmetric & S is transitive & S is antisymmetric implies R [*] S is antisymmetric )
set X = the carrier of (R [*] S);
set F = the InternalRel of (R [*] S);
assume that
A1: R tolerates S and
A2: the carrier of R /\ the carrier of S is upper Subset of R and
A3: the carrier of R /\ the carrier of S is lower Subset of S and
A4: ( R is transitive & R is antisymmetric ) and
A5: ( S is transitive & S is antisymmetric ) ; ::_thesis: R [*] S is antisymmetric
A6: the InternalRel of S is_antisymmetric_in the carrier of S by A5, ORDERS_2:def_4;
A7: the InternalRel of R is_antisymmetric_in the carrier of R by A4, ORDERS_2:def_4;
 the InternalRel of (R [*] S) is_antisymmetric_in the carrier of (R [*] S)
proof
let x, y be set ; :: according to RELAT_2:def_4 ::_thesis: ( not x in the carrier of (R [*] S) or not y in the carrier of (R [*] S) or not [x,y] in the InternalRel of (R [*] S) or not [y,x] in the InternalRel of (R [*] S) or x = y )
assume that
A8: ( x in the carrier of (R [*] S) & y in the carrier of (R [*] S) ) and
A9: [x,y] in the InternalRel of (R [*] S) and
A10: [y,x] in the InternalRel of (R [*] S) ; ::_thesis: x = y
A11: ( x in the carrier of R \/ the carrier of S & y in the carrier of R \/ the carrier of S ) by A8, Def2;
percases ( ( x in the carrier of R & y in the carrier of R ) or ( x in the carrier of R & y in the carrier of S ) or ( x in the carrier of S & y in the carrier of R ) or ( x in the carrier of S & y in the carrier of S ) ) by A11, XBOOLE_0:def_3;
supposeA12: ( x in the carrier of R & y in the carrier of R ) ; ::_thesis: x = y
then  ( [x,y] in the InternalRel of R & [y,x] in the InternalRel of R ) by A1, A4, A9, A10, Th4;
hence  x = y by A7, A12, RELAT_2:def_4; ::_thesis: verum
end;
supposeA13: ( x in the carrier of R & y in the carrier of S ) ; ::_thesis: x = y
then A14: y in the carrier of R by A3, A10, Th21;
then  ( [x,y] in the InternalRel of R & [y,x] in the InternalRel of R ) by A1, A4, A9, A10, A13, Th4;
hence  x = y by A7, A13, A14, RELAT_2:def_4; ::_thesis: verum
end;
supposeA15: ( x in the carrier of S & y in the carrier of R ) ; ::_thesis: x = y
then A16: y in the carrier of S by A2, A9, Th17;
then  ( [x,y] in the InternalRel of S & [y,x] in the InternalRel of S ) by A1, A5, A9, A10, A15, Th5;
hence  x = y by A6, A15, A16, RELAT_2:def_4; ::_thesis: verum
end;
supposeA17: ( x in the carrier of S & y in the carrier of S ) ; ::_thesis: x = y
then  ( [x,y] in the InternalRel of S & [y,x] in the InternalRel of S ) by A1, A5, A9, A10, Th5;
hence  x = y by A6, A17, RELAT_2:def_4; ::_thesis: verum
end;
end;
end;
hence  R [*] S is antisymmetric by ORDERS_2:def_4; ::_thesis: verum
end;

theorem :: LATSUM_1:25
for R, S being RelStr st the carrier of R /\ the carrier of S is upper Subset of R & the carrier of R /\ the carrier of S is lower Subset of S & R tolerates S & R is transitive & S is transitive holds
R [*] S is transitive
proof
let R, S be RelStr ; ::_thesis: ( the carrier of R /\ the carrier of S is upper Subset of R & the carrier of R /\ the carrier of S is lower Subset of S & R tolerates S & R is transitive & S is transitive implies R [*] S is transitive )
set X = the carrier of (R [*] S);
set F = the InternalRel of (R [*] S);
assume that
A1: the carrier of R /\ the carrier of S is upper Subset of R and
A2: the carrier of R /\ the carrier of S is lower Subset of S and
A3: R tolerates S and
A4: R is transitive and
A5: S is transitive ; ::_thesis: R [*] S is transitive
A6: the InternalRel of S is_transitive_in the carrier of S by A5, ORDERS_2:def_3;
A7: the InternalRel of R is_transitive_in the carrier of R by A4, ORDERS_2:def_3;
 the InternalRel of (R [*] S) is_transitive_in the carrier of (R [*] S)
proof
let x, y, z be set ; :: according to RELAT_2:def_8 ::_thesis: ( not x in the carrier of (R [*] S) or not y in the carrier of (R [*] S) or not z in the carrier of (R [*] S) or not [x,y] in the InternalRel of (R [*] S) or not [y,z] in the InternalRel of (R [*] S) or [x,z] in the InternalRel of (R [*] S) )
assume that
A8: ( x in the carrier of (R [*] S) & y in the carrier of (R [*] S) ) and
A9: z in the carrier of (R [*] S) and
A10: [x,y] in the InternalRel of (R [*] S) and
A11: [y,z] in the InternalRel of (R [*] S) ; ::_thesis: [x,z] in the InternalRel of (R [*] S)
A12: ( x in the carrier of R \/ the carrier of S & y in the carrier of R \/ the carrier of S ) by A8, Def2;
A13: z in the carrier of R \/ the carrier of S by A9, Def2;
percases ( ( x in the carrier of R & y in the carrier of R & z in the carrier of R ) or ( x in the carrier of R & y in the carrier of R & z in the carrier of S ) or ( x in the carrier of R & y in the carrier of S & z in the carrier of R ) or ( x in the carrier of S & y in the carrier of R & z in the carrier of R ) or ( x in the carrier of S & y in the carrier of S & z in the carrier of R ) or ( x in the carrier of S & y in the carrier of S & z in the carrier of S ) or ( x in the carrier of R & y in the carrier of S & z in the carrier of S ) or ( x in the carrier of S & y in the carrier of R & z in the carrier of S ) ) by A12, A13, XBOOLE_0:def_3;
supposeA14: ( x in the carrier of R & y in the carrier of R & z in the carrier of R ) ; ::_thesis: [x,z] in the InternalRel of (R [*] S)
then  ( [x,y] in the InternalRel of R & [y,z] in the InternalRel of R ) by A3, A4, A10, A11, Th4;
then  [x,z] in the InternalRel of R by A7, A14, RELAT_2:def_8;
hence  [x,z] in the InternalRel of (R [*] S) by Th6; ::_thesis: verum
end;
supposeA15: ( x in the carrier of R & y in the carrier of R & z in the carrier of S ) ; ::_thesis: [x,z] in the InternalRel of (R [*] S)
then A16: [x,y] in the InternalRel of R by A3, A4, A10, Th4;
 [y,z] in ( the InternalRel of R \/ the InternalRel of S) \/ ( the InternalRel of R * the InternalRel of S) by A11, Def2;
then A17: ( [y,z] in the InternalRel of R \/ the InternalRel of S or [y,z] in the InternalRel of R * the InternalRel of S ) by XBOOLE_0:def_3;
now__::_thesis:_[x,z]_in_the_InternalRel_of_(R_[*]_S)
percases ( [y,z] in the InternalRel of R or [y,z] in the InternalRel of S or [y,z] in the InternalRel of R * the InternalRel of S ) by A17, XBOOLE_0:def_3;
supposeA18: [y,z] in the InternalRel of R ; ::_thesis: [x,z] in the InternalRel of (R [*] S)
then  z in the carrier of R by ZFMISC_1:87;
then  [x,z] in the InternalRel of R by A7, A15, A16, A18, RELAT_2:def_8;
hence  [x,z] in the InternalRel of (R [*] S) by Th6; ::_thesis: verum
end;
suppose [y,z] in the InternalRel of S ; ::_thesis: [x,z] in the InternalRel of (R [*] S)
then  [x,z] in the InternalRel of R * the InternalRel of S by A16, RELAT_1:def_8;
then  [x,z] in ( the InternalRel of R \/ the InternalRel of S) \/ ( the InternalRel of R * the InternalRel of S) by XBOOLE_0:def_3;
hence  [x,z] in the InternalRel of (R [*] S) by Def2; ::_thesis: verum
end;
suppose [y,z] in the InternalRel of R * the InternalRel of S ; ::_thesis: [x,z] in the InternalRel of (R [*] S)
then consider a being set  such that
A19: [y,a] in the InternalRel of R and
A20: [a,z] in the InternalRel of S by RELAT_1:def_8;
 a in the carrier of R by A19, ZFMISC_1:87;
then  [x,a] in the InternalRel of R by A7, A15, A16, A19, RELAT_2:def_8;
then  [x,z] in the InternalRel of R * the InternalRel of S by A20, RELAT_1:def_8;
then  [x,z] in ( the InternalRel of R \/ the InternalRel of S) \/ ( the InternalRel of R * the InternalRel of S) by XBOOLE_0:def_3;
hence  [x,z] in the InternalRel of (R [*] S) by Def2; ::_thesis: verum
end;
end;
end;
hence  [x,z] in the InternalRel of (R [*] S) ; ::_thesis: verum
end;
supposeA21: ( x in the carrier of R & y in the carrier of S & z in the carrier of R ) ; ::_thesis: [x,z] in the InternalRel of (R [*] S)
then A22: y in the carrier of R by A2, A11, Th21;
then  ( [x,y] in the InternalRel of R & [y,z] in the InternalRel of R ) by A3, A4, A10, A11, A21, Th4;
then  [x,z] in the InternalRel of R by A7, A21, A22, RELAT_2:def_8;
hence  [x,z] in the InternalRel of (R [*] S) by Th6; ::_thesis: verum
end;
supposeA23: ( x in the carrier of S & y in the carrier of R & z in the carrier of R ) ; ::_thesis: [x,z] in the InternalRel of (R [*] S)
then A24: [y,z] in the InternalRel of R by A3, A4, A11, Th4;
A25: x in the carrier of R by A2, A10, A23, Th21;
then  [x,y] in the InternalRel of R by A3, A4, A10, A23, Th4;
then  [x,z] in the InternalRel of R by A7, A23, A25, A24, RELAT_2:def_8;
hence  [x,z] in the InternalRel of (R [*] S) by Th6; ::_thesis: verum
end;
supposeA26: ( x in the carrier of S & y in the carrier of S & z in the carrier of R ) ; ::_thesis: [x,z] in the InternalRel of (R [*] S)
then A27: [x,y] in the InternalRel of S by A3, A5, A10, Th5;
A28: z in the carrier of S by A1, A11, A26, Th17;
then  [y,z] in the InternalRel of S by A3, A5, A11, A26, Th5;
then  [x,z] in the InternalRel of S by A6, A26, A27, A28, RELAT_2:def_8;
hence  [x,z] in the InternalRel of (R [*] S) by Th6; ::_thesis: verum
end;
supposeA29: ( x in the carrier of S & y in the carrier of S & z in the carrier of S ) ; ::_thesis: [x,z] in the InternalRel of (R [*] S)
then  ( [x,y] in the InternalRel of S & [y,z] in the InternalRel of S ) by A3, A5, A10, A11, Th5;
then  [x,z] in the InternalRel of S by A6, A29, RELAT_2:def_8;
hence  [x,z] in the InternalRel of (R [*] S) by Th6; ::_thesis: verum
end;
supposeA30: ( x in the carrier of R & y in the carrier of S & z in the carrier of S ) ; ::_thesis: [x,z] in the InternalRel of (R [*] S)
then A31: [y,z] in the InternalRel of S by A3, A5, A11, Th5;
 [x,y] in ( the InternalRel of R \/ the InternalRel of S) \/ ( the InternalRel of R * the InternalRel of S) by A10, Def2;
then A32: ( [x,y] in the InternalRel of R \/ the InternalRel of S or [x,y] in the InternalRel of R * the InternalRel of S ) by XBOOLE_0:def_3;
now__::_thesis:_[x,z]_in_the_InternalRel_of_(R_[*]_S)
percases ( [x,y] in the InternalRel of R or [x,y] in the InternalRel of S or [x,y] in the InternalRel of R * the InternalRel of S ) by A32, XBOOLE_0:def_3;
suppose [x,y] in the InternalRel of R ; ::_thesis: [x,z] in the InternalRel of (R [*] S)
then  [x,z] in the InternalRel of R * the InternalRel of S by A31, RELAT_1:def_8;
then  [x,z] in ( the InternalRel of R \/ the InternalRel of S) \/ ( the InternalRel of R * the InternalRel of S) by XBOOLE_0:def_3;
hence  [x,z] in the InternalRel of (R [*] S) by Def2; ::_thesis: verum
end;
supposeA33: [x,y] in the InternalRel of S ; ::_thesis: [x,z] in the InternalRel of (R [*] S)
then  x in the carrier of S by ZFMISC_1:87;
then  [x,z] in the InternalRel of S by A6, A30, A31, A33, RELAT_2:def_8;
hence  [x,z] in the InternalRel of (R [*] S) by Th6; ::_thesis: verum
end;
suppose [x,y] in the InternalRel of R * the InternalRel of S ; ::_thesis: [x,z] in the InternalRel of (R [*] S)
then consider a being set  such that
A34: [x,a] in the InternalRel of R and
A35: [a,y] in the InternalRel of S by RELAT_1:def_8;
 a in the carrier of S by A35, ZFMISC_1:87;
then  [a,z] in the InternalRel of S by A6, A30, A31, A35, RELAT_2:def_8;
then  [x,z] in the InternalRel of R * the InternalRel of S by A34, RELAT_1:def_8;
then  [x,z] in ( the InternalRel of R \/ the InternalRel of S) \/ ( the InternalRel of R * the InternalRel of S) by XBOOLE_0:def_3;
hence  [x,z] in the InternalRel of (R [*] S) by Def2; ::_thesis: verum
end;
end;
end;
hence  [x,z] in the InternalRel of (R [*] S) ; ::_thesis: verum
end;
supposeA36: ( x in the carrier of S & y in the carrier of R & z in the carrier of S ) ; ::_thesis: [x,z] in the InternalRel of (R [*] S)
then A37: y in the carrier of S by A1, A10, Th17;
then  ( [x,y] in the InternalRel of S & [y,z] in the InternalRel of S ) by A3, A5, A10, A11, A36, Th5;
then  [x,z] in the InternalRel of S by A6, A36, A37, RELAT_2:def_8;
hence  [x,z] in the InternalRel of (R [*] S) by Th6; ::_thesis: verum
end;
end;
end;
hence  R [*] S is transitive by ORDERS_2:def_3; ::_thesis: verum
end;