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