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

set a = the Element of Y;
A2: the Element of Y <= the Element of Y ;
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, 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; :: 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

set a = the Element of X;
A3: the Element of X <= the Element of X ;
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 ( [ 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; :: thesis: verum

end;

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