let x, y be object ; :: according to RELAT_2:def 4,ORDERS_2:def 4 :: 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 object 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 object 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 ;
then [(y `1),(x `1)] in the InternalRel of X ;
then [y1,([x1,x2] `1)] in the InternalRel of X by A7, A10;
then A12: [y1,x1] in the InternalRel of X ;
[(([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 ;
then [(y `2),(x `2)] in the InternalRel of Y ;
then [y2,([x1,x2] `2)] in the InternalRel of Y by A7, A10;
then A13: [y2,x2] in the InternalRel of Y ;
A14: [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 ;
then [(x `2),(y `2)] in the InternalRel of Y ;
then [x2,([y1,y2] `2)] in the InternalRel of Y by A7, A10;
then A15: [x2,y2] in the InternalRel of Y ;
[(([x,y] `1) `1),(([x,y] `2) `1)] in the InternalRel of X by A14, 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,([y1,y2] `1)] in the InternalRel of X by A7, A10;
then [x1,y1] in the InternalRel of X ;
then ( the InternalRel of Y is_antisymmetric_in the carrier of Y & x1 = y1 ) by A5, A8, A12, ORDERS_2:def 4, RELAT_2:def 4;
hence x = y by A6, A7, A9, A10, A15, A13; :: thesis: verum