let A be Preorder; :: thesis: for B being Subset of A st the InternalRel of A is_connected_in B holds
the InternalRel of (QuotientOrder A) is_connected_in (proj A) .: B
let B be Subset of A; :: thesis: ( the InternalRel of A is_connected_in B implies the InternalRel of (QuotientOrder A) is_connected_in (proj A) .: B )
set qa = QuotientOrder A;
set car = the carrier of A;
set carq = the carrier of (QuotientOrder A);
set int = the InternalRel of A;
set intq = the InternalRel of (QuotientOrder A);
set C = (proj A) .: B;
assume A1: the InternalRel of A is_connected_in B ; :: thesis: the InternalRel of (QuotientOrder A) is_connected_in (proj A) .: B
for X, Y being object st X in (proj A) .: B & Y in (proj A) .: B & X <> Y & not [X,Y] in the InternalRel of (QuotientOrder A) holds
[Y,X] in the InternalRel of (QuotientOrder A)

proof

let X, Y be object ; :: thesis: ( X in (proj A) .: B & Y in (proj A) .: B & X <> Y & not [X,Y] in the InternalRel of (QuotientOrder A) implies [Y,X] in the InternalRel of (QuotientOrder A) )
assume that
A2: ( X in (proj A) .: B & Y in (proj A) .: B ) and
A3: X <> Y ; :: thesis: ( [X,Y] in the InternalRel of (QuotientOrder A) or [Y,X] in the InternalRel of (QuotientOrder A) )
consider x being object such that
A4: x in dom (proj A) and
A5: x in B and
A6: X = (proj A) . x by A2, FUNCT_1:def 6;
consider y being object such that
A7: y in dom (proj A) and
A8: y in B and
A9: Y = (proj A) . y by A2, FUNCT_1:def 6;

per cases ( A is empty or not A is empty ) ;

suppose A is empty ; :: thesis: ( [X,Y] in the InternalRel of (QuotientOrder A) or [Y,X] in the InternalRel of (QuotientOrder A) )

hence ( [X,Y] in the InternalRel of (QuotientOrder A) or [Y,X] in the InternalRel of (QuotientOrder A) ) by A2; :: thesis: verum

end;

suppose not A is empty ; :: thesis: ( [X,Y] in the InternalRel of (QuotientOrder A) or [Y,X] in the InternalRel of (QuotientOrder A) )

then reconsider A = A as non empty Preorder ;
reconsider x = x, y = y as Element of A by A4, A7;
x <> y by A3, A6, A9;
then ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) by A1, A5, A8, RELAT_2:def 6;
then ( (proj A) . x <= (proj A) . y or (proj A) . y <= (proj A) . x ) by Th45, ORDERS_2:def 5;
hence ( [X,Y] in the InternalRel of (QuotientOrder A) or [Y,X] in the InternalRel of (QuotientOrder A) ) by A6, A9, ORDERS_2:def 5; :: thesis: verum

end;

end;

end;

hence the InternalRel of (QuotientOrder A) is_connected_in (proj A) .: B by RELAT_2:def 6; :: thesis: verum