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

end;

suppose
not A is empty
; :: thesis: eqSupport (f,X) is trivial

then
X in the carrier of (QuotientOrder A)
by SUBSET_1:def 1;

then X in Class (EqRelOf A) by Def7;

then consider x being object such that

A1: x in the carrier of A and

A2: X = Class ((EqRelOf A),x) by EQREL_1:def 3;

X = Class ((id the carrier of A),x) by A2, Th42

.= {x} by A1, EQREL_1:25 ;

hence eqSupport (f,X) is trivial by XBOOLE_1:17, ZFMISC_1:33; :: thesis: verum

end;then X in Class (EqRelOf A) by Def7;

then consider x being object such that

A1: x in the carrier of A and

A2: X = Class ((EqRelOf A),x) by EQREL_1:def 3;

X = Class ((id the carrier of A),x) by A2, Th42

.= {x} by A1, EQREL_1:25 ;

hence eqSupport (f,X) is trivial by XBOOLE_1:17, ZFMISC_1:33; :: thesis: verum