let x, y, z be set ; :: according to RELAT_2:def 8,ORDERS_2:def 5 :: thesis: ( not x in the carrier of [:X,Y:] or not y in the carrier of [:X,Y:] or not z in the carrier of [:X,Y:] or not [x,y] in the InternalRel of [:X,Y:] or not [y,z] in the InternalRel of [:X,Y:] or [x,z] in the InternalRel of [:X,Y:] )
assume that
A1: x in the carrier of [:X,Y:] and
A2: y in the carrier of [:X,Y:] and
A3: z in the carrier of [:X,Y:] and
A4: [x,y] in the InternalRel of [:X,Y:] and
A5: [y,z] in the InternalRel of [:X,Y:] ; :: thesis: [x,z] in the InternalRel of [:X,Y:]
x in [:the carrier of X,the carrier of Y:] by A1, Def2;
then consider x1, x2 being set such that
A6: ( x1 in the carrier of X & x2 in the carrier of Y & x = [x1,x2] ) by ZFMISC_1:def 2;
y in [:the carrier of X,the carrier of Y:] by A2, Def2;
then consider y1, y2 being set such that
A7: ( y1 in the carrier of X & y2 in the carrier of Y & y = [y1,y2] ) by ZFMISC_1:def 2;
z in [:the carrier of X,the carrier of Y:] by A3, Def2;
then consider z1, z2 being set such that
A8: ( z1 in the carrier of X & z2 in the carrier of Y & z = [z1,z2] ) by ZFMISC_1:def 2;
set P = the InternalRel of X;
set R = the InternalRel of Y;
A9: ( the InternalRel of X is_transitive_in the carrier of X & the InternalRel of Y is_transitive_in the carrier of Y ) by ORDERS_2:def 5;
[x,y] in ["the InternalRel of X,the InternalRel of Y"] by A4, Def2;
then ( [(([x,y] `1 ) `1 ),(([x,y] `2 ) `1 )] in the InternalRel of X & [(([x,y] `1 ) `2 ),(([x,y] `2 ) `2 )] in the InternalRel of Y ) by Th10;
then ( [(x `1 ),(([x,y] `2 ) `1 )] in the InternalRel of X & [(x `2 ),(([x,y] `2 ) `2 )] in the InternalRel of Y ) by MCART_1:7;
then ( [(x `1 ),(y `1 )] in the InternalRel of X & [(x `2 ),(y `2 )] in the InternalRel of Y ) by MCART_1:7;
then ( [x1,(y `1 )] in the InternalRel of X & [x2,(y `2 )] in the InternalRel of Y ) by A6, MCART_1:7;
then A10: ( [x1,y1] in the InternalRel of X & [x2,y2] in the InternalRel of Y ) by A7, MCART_1:7;
[y,z] in ["the InternalRel of X,the InternalRel of Y"] by A5, Def2;
then ( [(([y,z] `1 ) `1 ),(([y,z] `2 ) `1 )] in the InternalRel of X & [(([y,z] `1 ) `2 ),(([y,z] `2 ) `2 )] in the InternalRel of Y ) by Th10;
then ( [(y `1 ),(([y,z] `2 ) `1 )] in the InternalRel of X & [(y `2 ),(([y,z] `2 ) `2 )] in the InternalRel of Y ) by MCART_1:7;
then ( [(y `1 ),(z `1 )] in the InternalRel of X & [(y `2 ),(z `2 )] in the InternalRel of Y ) by MCART_1:7;
then ( [y1,(z `1 )] in the InternalRel of X & [y2,(z `2 )] in the InternalRel of Y ) by A7, MCART_1:7;
then ( [y1,z1] in the InternalRel of X & [y2,z2] in the InternalRel of Y ) by A8, MCART_1:7;
then ( [x1,z1] in the InternalRel of X & [x2,z2] in the InternalRel of Y ) by A6, A7, A8, A9, A10, RELAT_2:def 8;
then ( [x1,(z `1 )] in the InternalRel of X & [x2,(z `2 )] in the InternalRel of Y ) by A8, MCART_1:7;
then A11: ( [(x `1 ),(z `1 )] in the InternalRel of X & [(x `2 ),(z `2 )] in the InternalRel of Y ) by A6, MCART_1:7;
( [x,z] `1 = x & [x,z] `2 = z ) by MCART_1:7;
then [x,z] in ["the InternalRel of X,the InternalRel of Y"] by A6, A8, A11, Th10;
hence [x,z] in the InternalRel of [:X,Y:] by Def2; :: thesis: verum