A1: R = EqRelOf A by Def9;

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

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;

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;

end;