set qa = QuotientOrder A;
set car = the carrier of ();
set int = the InternalRel of ();
for X, Y being object st X in the carrier of () & Y in the carrier of () & 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 the carrier of () & Y in the carrier of () & X <> Y & not [X,Y] in the InternalRel of () implies [Y,X] in the InternalRel of () )
assume that
A1: ( X in the carrier of () & Y in the carrier of () ) and
X <> Y ; :: thesis: ( [X,Y] in the InternalRel of () or [Y,X] in the InternalRel of () )
reconsider X = X, Y = Y as Element of Class () by ;
A2: ( X in Class () & Y in Class () ) by ;
consider x being object such that
A3: x in the carrier of A and
A4: X = Class ((),x) by ;
consider y being object such that
A5: y in the carrier of A and
A6: Y = Class ((),y) by ;
reconsider x = x, y = y as Element of A by A3, A5;
not A is empty by A3;
per cases then ( x <= y or y <= x ) by Th25;
suppose x <= y ; :: 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 A4, A6, Def7; :: thesis: verum
end;
suppose y <= x ; :: 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 A4, A6, Def7; :: thesis: verum
end;
end;
end;
hence QuotientOrder A is connected by RELAT_2:def 6; :: thesis:
hence QuotientOrder A is strongly_connected ; :: thesis: verum