let A be Preorder; :: thesis: for B being Subset of A st the InternalRel of A is_connected_in B holds
the InternalRel of () 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 () is_connected_in (proj A) .: B )
set qa = QuotientOrder A;
set car = the carrier of A;
set carq = the carrier of ();
set int = the InternalRel of A;
set intq = the InternalRel of ();
set C = (proj A) .: B;
assume A1: the InternalRel of A is_connected_in B ; :: thesis: the InternalRel of () 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 () holds
[Y,X] in the InternalRel of ()
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 () implies [Y,X] in the InternalRel of () )
assume that
A2: ( X in (proj A) .: B & Y in (proj A) .: B ) and
A3: X <> Y ; :: thesis: ( [X,Y] in the InternalRel of () or [Y,X] in the InternalRel of () )
consider x being object such that
A4: x in dom (proj A) and
A5: x in B and
A6: X = (proj A) . x by ;
consider y being object such that
A7: y in dom (proj A) and
A8: y in B and
A9: Y = (proj A) . y by ;
per cases ( A is empty or not A is empty ) ;
suppose A is empty ; :: thesis: ( [X,Y] in the InternalRel of () or [Y,X] in the InternalRel of () )
hence ( [X,Y] in the InternalRel of () or [Y,X] in the InternalRel of () ) by A2; :: thesis: verum
end;
suppose not A is empty ; :: thesis: ( [X,Y] in the InternalRel of () or [Y,X] in the InternalRel of () )
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 ;
then ( (proj A) . x <= (proj A) . y or (proj A) . y <= (proj A) . x ) by ;
hence ( [X,Y] in the InternalRel of () or [Y,X] in the InternalRel of () ) by ; :: thesis: verum
end;
end;
end;
hence the InternalRel of () is_connected_in (proj A) .: B by RELAT_2:def 6; :: thesis: verum