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:] & [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
A4: ( 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
A5: ( y1 in the carrier of X & y2 in the carrier of Y & y = [y1,y2] ) by ZFMISC_1:def 2;
[x,y] in ["the InternalRel of X,the InternalRel of Y"] by A3, 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,([y1,y2] `1 )] in the InternalRel of X & [x2,([y1,y2] `2 )] in the InternalRel of Y ) by A4, A5, MCART_1:7;
then A6: ( [x1,y1] in the InternalRel of X & [x2,y2] in the InternalRel of Y ) by MCART_1:7;
[y,x] in ["the InternalRel of X,the InternalRel of Y"] by A3, Def2;
then ( [(([y,x] `1 ) `1 ),(([y,x] `2 ) `1 )] in the InternalRel of X & [(([y,x] `1 ) `2 ),(([y,x] `2 ) `2 )] in the InternalRel of Y ) by Th10;
then ( [(y `1 ),(([y,x] `2 ) `1 )] in the InternalRel of X & [(y `2 ),(([y,x] `2 ) `2 )] in the InternalRel of Y ) by MCART_1:7;
then ( [(y `1 ),(x `1 )] in the InternalRel of X & [(y `2 ),(x `2 )] in the InternalRel of Y ) by MCART_1:7;
then ( [y1,([x1,x2] `1 )] in the InternalRel of X & [y2,([x1,x2] `2 )] in the InternalRel of Y ) by A4, A5, MCART_1:7;
then A7: ( [y1,x1] in the InternalRel of X & [y2,x2] in the InternalRel of Y ) by MCART_1:7;
( the InternalRel of X is_antisymmetric_in the carrier of X & the InternalRel of Y is_antisymmetric_in the carrier of Y ) by ORDERS_2:def 6;
then ( x1 = y1 & x2 = y2 ) by A4, A5, A6, A7, RELAT_2:def 4;
hence x = y by A4, A5; :: thesis: verum