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)

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

hence
the InternalRel of (QuotientOrder A) is_connected_in (proj A) .: B
by RELAT_2:def 6; :: thesis: verum
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;

end;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 )
;

end;

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;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