let x be object ; :: according to RELAT_2:def 1,ORDERS_2:def 2 :: thesis: ( not x in the carrier of [:X,Y:] or [x,x] in the InternalRel of [:X,Y:] )
assume x in the carrier of [:X,Y:] ; :: thesis: [x,x] in the InternalRel of [:X,Y:]
then x in [: the carrier of X, the carrier of Y:] by Def2;
then consider x1, x2 being object such that
A1: x1 in the carrier of X and
A2: x2 in the carrier of Y and
A3: x = [x1,x2] by ZFMISC_1:def 2;
the InternalRel of X is_reflexive_in the carrier of X by ORDERS_2:def 2;
then A4: [x1,x1] in the InternalRel of X by A1;
the InternalRel of Y is_reflexive_in the carrier of Y by ORDERS_2:def 2;
then A5: [x2,x2] in the InternalRel of Y by A2;
set a = [[x1,x2],[x1,x2]];
A6: ( [[x1,x2],[x1,x2]] `1 = [x1,x2] & [[x1,x2],[x1,x2]] `2 = [x1,x2] ) ;
( ([[x1,x2],[x1,x2]] `1) `1 = x1 & ([[x1,x2],[x1,x2]] `1) `2 = x2 ) ;
then [x,x] in [" the InternalRel of X, the InternalRel of Y"] by A3, A4, A5, A6, Th10;
hence [x,x] in the InternalRel of [:X,Y:] by Def2; :: thesis: verum