let X, Y be non empty reflexive RelStr ; :: thesis: ( [:X,Y:] is transitive implies ( X is transitive & Y is transitive ) )
assume A1: [:X,Y:] is transitive ; :: thesis: ( X is transitive & Y is transitive )
for x, y, z being Element of X st x <= y & y <= z holds
x <= z

proof

consider a being Element of Y;
A2: a <= a ;
let x, y, z be Element of X; :: thesis: ( x <= y & y <= z implies x <= z )
assume ( x <= y & y <= z ) ; :: thesis: x <= z
then ( [x,a] <= [y,a] & [y,a] <= [z,a] ) by A2, Th11;
then [x,a] <= [z,a] by A1, YELLOW_0:def 2;
hence x <= z by Th11; :: thesis: verum

end;

hence X is transitive by YELLOW_0:def 2; :: thesis: Y is transitive
for x, y, z being Element of Y st x <= y & y <= z holds
x <= z

proof

consider a being Element of X;
A3: a <= a ;
let x, y, z be Element of Y; :: thesis: ( x <= y & y <= z implies x <= z )
assume ( x <= y & y <= z ) ; :: thesis: x <= z
then ( [a,x] <= [a,y] & [a,y] <= [a,z] ) by A3, Th11;
then [a,x] <= [a,z] by A1, YELLOW_0:def 2;
hence x <= z by Th11; :: thesis: verum

end;

hence Y is transitive by YELLOW_0:def 2; :: thesis: verum