A1:
R = EqRelOf A
by Def9;

per cases
( not A is empty or A is empty )
;

end;

suppose
not A is empty
; :: thesis: Im (R,x) is Element of (QuotientOrder A)

then reconsider A = A as non empty Preorder ;

Class (R,x) in the carrier of (QuotientOrder A) by A1, Th43;

hence Im (R,x) is Element of (QuotientOrder A) ; :: thesis: verum

end;Class (R,x) in the carrier of (QuotientOrder A) by A1, Th43;

hence Im (R,x) is Element of (QuotientOrder A) ; :: thesis: verum

suppose
A is empty
; :: thesis: Im (R,x) is Element of (QuotientOrder A)

then reconsider A = A as empty Preorder ;

EqRelOf A is empty ;

then A2: Class (R,x) = {} ;

{} is Element of (QuotientOrder A) by SUBSET_1:def 1;

hence Im (R,x) is Element of (QuotientOrder A) by A2; :: thesis: verum

end;EqRelOf A is empty ;

then A2: Class (R,x) = {} ;

{} is Element of (QuotientOrder A) by SUBSET_1:def 1;

hence Im (R,x) is Element of (QuotientOrder A) by A2; :: thesis: verum