let X, Y be non empty reflexive RelStr ; ( [:X,Y:] is transitive implies ( X is transitive & Y is transitive ) )
assume A1:
[:X,Y:] is transitive
; ( X is transitive & Y is transitive )
for x, y, z being Element of X st x <= y & y <= z holds
x <= z
proof
set a = the
Element of
Y;
A2:
the
Element of
Y <= the
Element of
Y
;
let x,
y,
z be
Element of
X;
( x <= y & y <= z implies x <= z )
assume
(
x <= y &
y <= z )
;
x <= z
then
(
[x, the Element of Y] <= [y, the Element of Y] &
[y, the Element of Y] <= [z, the Element of Y] )
by A2, Th11;
then
[x, the Element of Y] <= [z, the Element of Y]
by A1, YELLOW_0:def 2;
hence
x <= z
by Th11;
verum
end;
hence
X is transitive
by YELLOW_0:def 2; Y is transitive
for x, y, z being Element of Y st x <= y & y <= z holds
x <= z
proof
set a = the
Element of
X;
A3:
the
Element of
X <= the
Element of
X
;
let x,
y,
z be
Element of
Y;
( x <= y & y <= z implies x <= z )
assume
(
x <= y &
y <= z )
;
x <= z
then
(
[ the Element of X,x] <= [ the Element of X,y] &
[ the Element of X,y] <= [ the Element of X,z] )
by A3, Th11;
then
[ the Element of X,x] <= [ the Element of X,z]
by A1, YELLOW_0:def 2;
hence
x <= z
by Th11;
verum
end;
hence
Y is transitive
by YELLOW_0:def 2; verum