let R, S be RelStr ; ( 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
; 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
object ;
RELAT_2:def 8 ( 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)
;
[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;
per cases
( ( 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;
suppose A15:
(
x in the
carrier of
R &
y in the
carrier of
R &
z in the
carrier of
S )
;
[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 [x,z] in the InternalRel of (R [*] S)per cases
( [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;
suppose
[y,z] in the
InternalRel of
R * the
InternalRel of
S
;
[x,z] in the InternalRel of (R [*] S)then consider a being
object 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;
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;
verum end; end; end; hence
[x,z] in the
InternalRel of
(R [*] S)
;
verum end; suppose A21:
(
x in the
carrier of
R &
y in the
carrier of
S &
z in the
carrier of
R )
;
[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;
hence
[x,z] in the
InternalRel of
(R [*] S)
by Th6;
verum end; suppose A23:
(
x in the
carrier of
S &
y in the
carrier of
R &
z in the
carrier of
R )
;
[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;
hence
[x,z] in the
InternalRel of
(R [*] S)
by Th6;
verum end; suppose A26:
(
x in the
carrier of
S &
y in the
carrier of
S &
z in the
carrier of
R )
;
[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;
hence
[x,z] in the
InternalRel of
(R [*] S)
by Th6;
verum end; suppose A30:
(
x in the
carrier of
R &
y in the
carrier of
S &
z in the
carrier of
S )
;
[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 [x,z] in the InternalRel of (R [*] S)per cases
( [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 * the
InternalRel of
S
;
[x,z] in the InternalRel of (R [*] S)then consider a being
object 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;
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;
verum end; end; end; hence
[x,z] in the
InternalRel of
(R [*] S)
;
verum end; suppose A36:
(
x in the
carrier of
S &
y in the
carrier of
R &
z in the
carrier of
S )
;
[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;
hence
[x,z] in the
InternalRel of
(R [*] S)
by Th6;
verum end; end;
end;
hence
R [*] S is transitive
by ORDERS_2:def 3; verum