set R = the InternalRel of [:P,Q:];
reconsider L = L as Relation of the carrier of P, the carrier of Q by YELLOW_3:def 2;
reconsider L1 = dom L as Subset of P ;
reconsider L2 = rng L as Subset of Q ;
set R1 = the InternalRel of P;
for x, y being object st x in L1 & y in L1 & not [x,y] in the InternalRel of P holds
[y,x] in the InternalRel of P

proof

let x, y be object ; :: thesis: ( x in L1 & y in L1 & not [x,y] in the InternalRel of P implies [y,x] in the InternalRel of P )
assume B1: ( x in L1 & y in L1 ) ; :: thesis: ( [x,y] in the InternalRel of P or [y,x] in the InternalRel of P )
then reconsider x = x, y = y as Element of P ;
consider q1 being object such that
B2: [x,q1] in L by XTUPLE_0:def 12, B1;
consider q2 being object such that
B3: [y,q2] in L by XTUPLE_0:def 12, B1;
( q1 in L2 & q2 in L2 ) by B2, B3, XTUPLE_0:def 13;
then reconsider q1 = q1, q2 = q2 as Element of Q ;
reconsider a = [x,q1] as Element of [:P,Q:] ;
reconsider b = [y,q2] as Element of [:P,Q:] ;

per cases ( a <= b or b <= a ) by ORDERS_2:def 7, RELAT_2:def 7, B2, B3;

suppose a <= b ; :: thesis: ( [x,y] in the InternalRel of P or [y,x] in the InternalRel of P )

then x <= y by YELLOW_3:11;
hence ( [x,y] in the InternalRel of P or [y,x] in the InternalRel of P ) ; :: thesis: verum

end;

suppose b <= a ; :: thesis: ( [x,y] in the InternalRel of P or [y,x] in the InternalRel of P )

then y <= x by YELLOW_3:11;
hence ( [x,y] in the InternalRel of P or [y,x] in the InternalRel of P ) ; :: thesis: verum

end;

end;

end;

hence dom L is non empty Chain of P by ORDERS_2:def 7, RELAT_2:def 7; :: thesis: verum