let A be Preorder; 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; ( 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
; 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 ;
( 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
;
( [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
not
A is
empty
;
( [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;
verum end;
end;
hence
the InternalRel of (QuotientOrder A) is_connected_in (proj A) .: B
by RELAT_2:def 6; verum