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)

hence QuotientOrder A is strongly_connected ; :: thesis: verum

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

hence
QuotientOrder A is connected
by RELAT_2:def 6; :: thesis: QuotientOrder A is strongly_connected
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;

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

end;

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;hence QuotientOrder A is strongly_connected ; :: thesis: verum