set P = the InternalRel of X;
set R = the InternalRel of Y;
let x, y, z be object ; :: according to RELAT_2:def 8,ORDERS_2:def 3 :: 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:]
y in [: the carrier of X, the carrier of Y:] by A2, Def2;
then consider y1, y2 being object such that
A6: y1 in the carrier of X and
A7: y2 in the carrier of Y and
A8: 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 object such that
A9: z1 in the carrier of X and
A10: z2 in the carrier of Y and
A11: z = [z1,z2] by ZFMISC_1:def 2;
A12: [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 by Th10;
then [(y `1),(([y,z] `2) `1)] in the InternalRel of X ;
then [(y `1),(z `1)] in the InternalRel of X ;
then [y1,(z `1)] in the InternalRel of X by A8;
then A13: [y1,z1] in the InternalRel of X by A11;
x in [: the carrier of X, the carrier of Y:] by A1, Def2;
then consider x1, x2 being object such that
A14: x1 in the carrier of X and
A15: x2 in the carrier of Y and
A16: x = [x1,x2] by ZFMISC_1:def 2;
A17: [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 by Th10;
then [(x `1),(([x,y] `2) `1)] in the InternalRel of X ;
then [(x `1),(y `1)] in the InternalRel of X ;
then [x1,(y `1)] in the InternalRel of X by A16;
then ( the InternalRel of X is_transitive_in the carrier of X & [x1,y1] in the InternalRel of X ) by A8, ORDERS_2:def 3;
then [x1,z1] in the InternalRel of X by A14, A6, A9, A13;
then [x1,(z `1)] in the InternalRel of X by A11;
then A18: [(x `1),(z `1)] in the InternalRel of X by A16;
[(([y,z] `1) `2),(([y,z] `2) `2)] in the InternalRel of Y by A12, Th10;
then [(y `2),(([y,z] `2) `2)] in the InternalRel of Y ;
then [(y `2),(z `2)] in the InternalRel of Y ;
then [y2,(z `2)] in the InternalRel of Y by A8;
then A19: [y2,z2] in the InternalRel of Y by A11;
[(([x,y] `1) `2),(([x,y] `2) `2)] in the InternalRel of Y by A17, Th10;
then [(x `2),(([x,y] `2) `2)] in the InternalRel of Y ;
then [(x `2),(y `2)] in the InternalRel of Y ;
then [x2,(y `2)] in the InternalRel of Y by A16;
then ( the InternalRel of Y is_transitive_in the carrier of Y & [x2,y2] in the InternalRel of Y ) by A8, ORDERS_2:def 3;
then [x2,z2] in the InternalRel of Y by A15, A7, A10, A19;
then [x2,(z `2)] in the InternalRel of Y by A11;
then A20: [(x `2),(z `2)] in the InternalRel of Y by A16;
( [x,z] `1 = x & [x,z] `2 = z ) ;
then [x,z] in [" the InternalRel of X, the InternalRel of Y"] by A16, A11, A18, A20, Th10;
hence [x,z] in the InternalRel of [:X,Y:] by Def2; :: thesis: verum