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 R2 = the InternalRel of Q;
for x, y being object st x in L2 & y in L2 & not [x,y] in the InternalRel of Q holds
[y,x] in the InternalRel of Q
proof
let x, y be object ; :: thesis: ( x in L2 & y in L2 & not [x,y] in the InternalRel of Q implies [y,x] in the InternalRel of Q )
assume B1: ( x in L2 & y in L2 ) ; :: thesis: ( [x,y] in the InternalRel of Q or [y,x] in the InternalRel of Q )
then reconsider x = x, y = y as Element of Q ;
consider p1 being object such that
B2: [p1,x] in L by XTUPLE_0:def 13, B1;
consider p2 being object such that
B3: [p2,y] in L by XTUPLE_0:def 13, B1;
( p1 in L1 & p2 in L1 ) by B2, B3, XTUPLE_0:def 12;
then reconsider p1 = p1, p2 = p2 as Element of P ;
reconsider a = [p1,x], b = [p2,y] 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 Q or [y,x] in the InternalRel of Q )
then x <= y by YELLOW_3:11;
hence ( [x,y] in the InternalRel of Q or [y,x] in the InternalRel of Q ) ; :: thesis: verum
end;
suppose b <= a ; :: thesis: ( [x,y] in the InternalRel of Q or [y,x] in the InternalRel of Q )
then y <= x by YELLOW_3:11;
hence ( [x,y] in the InternalRel of Q or [y,x] in the InternalRel of Q ) ; :: thesis: verum
end;
end;
end;
hence rng L is non empty Chain of Q by ORDERS_2:def 7, RELAT_2:def 7; :: thesis: verum