let x, y be set ; :: according to RELAT_2:def 4,ORDERS_2:def 6 :: thesis: ( not x in the carrier of [:X,Y:] or not y in the carrier of [:X,Y:] or not [x,y] in the InternalRel of [:X,Y:] or not [y,x] in the InternalRel of [:X,Y:] or x = y )
assume that
A1: x in the carrier of [:X,Y:] and
A2: y in the carrier of [:X,Y:] and
A3: [x,y] in the InternalRel of [:X,Y:] and
A4: [y,x] in the InternalRel of [:X,Y:] ; :: thesis: x = y
x in [:the carrier of X,the carrier of Y:] by A1, Def2;
then consider x1, x2 being set such that
A5: x1 in the carrier of X and
A6: x2 in the carrier of Y and
A7: 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
A8: y1 in the carrier of X and
A9: y2 in the carrier of Y and
A10: y = [y1,y2] by ZFMISC_1:def 2;
A11: [y,x] in ["the InternalRel of X,the InternalRel of Y"] by A4, Def2;
then [(([y,x] `1 ) `1 ),(([y,x] `2 ) `1 )] in the InternalRel of X by Th10;
then [(y `1 ),(([y,x] `2 ) `1 )] in the InternalRel of X by MCART_1:7;
then [(y `1 ),(x `1 )] in the InternalRel of X by MCART_1:7;
then [y1,([x1,x2] `1 )] in the InternalRel of X by A7, A10, MCART_1:7;
then A12: [y1,x1] in the InternalRel of X by MCART_1:7;
[(([y,x] `1 ) `2 ),(([y,x] `2 ) `2 )] in the InternalRel of Y by A11, Th10;
then [(y `2 ),(([y,x] `2 ) `2 )] in the InternalRel of Y by MCART_1:7;
then [(y `2 ),(x `2 )] in the InternalRel of Y by MCART_1:7;
then [y2,([x1,x2] `2 )] in the InternalRel of Y by A7, A10, MCART_1:7;
then A13: [y2,x2] in the InternalRel of Y by MCART_1:7;
A14: the InternalRel of X is_antisymmetric_in the carrier of X by ORDERS_2:def 6;
A15: [x,y] in ["the InternalRel of X,the InternalRel of Y"] by A3, Def2;
then [(([x,y] `1 ) `2 ),(([x,y] `2 ) `2 )] in the InternalRel of Y by Th10;
then [(x `2 ),(([x,y] `2 ) `2 )] in the InternalRel of Y by MCART_1:7;
then [(x `2 ),(y `2 )] in the InternalRel of Y by MCART_1:7;
then [x2,([y1,y2] `2 )] in the InternalRel of Y by A7, A10, MCART_1:7;
then A16: [x2,y2] in the InternalRel of Y by MCART_1:7;
[(([x,y] `1 ) `1 ),(([x,y] `2 ) `1 )] in the InternalRel of X by A15, Th10;
then [(x `1 ),(([x,y] `2 ) `1 )] in the InternalRel of X by MCART_1:7;
then [(x `1 ),(y `1 )] in the InternalRel of X by MCART_1:7;
then [x1,([y1,y2] `1 )] in the InternalRel of X by A7, A10, MCART_1:7;
then [x1,y1] in the InternalRel of X by MCART_1:7;
then ( the InternalRel of Y is_antisymmetric_in the carrier of Y & x1 = y1 ) by A5, A8, A12, A14, ORDERS_2:def 6, RELAT_2:def 4;
hence x = y by A6, A7, A9, A10, A16, A13, RELAT_2:def 4; :: thesis: verum