let x be set ; :: according to RELAT_2:def 1,ORDERS_2:def 4 :: 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 set such that
A1: ( x1 in the carrier of X & x2 in the carrier of Y & x = [x1,x2] ) by ZFMISC_1:def 2;
set a = [[x1,x2],[x1,x2]];
( the InternalRel of X is_reflexive_in the carrier of X & the InternalRel of Y is_reflexive_in the carrier of Y ) by ORDERS_2:def 4;
then A2: ( [x1,x1] in the InternalRel of X & [x2,x2] in the InternalRel of Y ) by A1, RELAT_2:def 1;
A3: ( [[x1,x2],[x1,x2]] `1 = [x1,x2] & [[x1,x2],[x1,x2]] `2 = [x1,x2] ) by MCART_1:7;
( ([[x1,x2],[x1,x2]] `1 ) `1 = x1 & ([[x1,x2],[x1,x2]] `1 ) `2 = x2 & ([[x1,x2],[x1,x2]] `2 ) `1 = x1 & ([[x1,x2],[x1,x2]] `2 ) `2 = x2 ) by Lm1;
then [x,x] in ["the InternalRel of X,the InternalRel of Y"] by A1, A2, A3, Th10;
hence [x,x] in the InternalRel of [:X,Y:] by Def2; :: thesis: verum