let R be non empty Poset; :: thesis: for x being Element of R holds Class ((EqRel R),x) = {x}
set IR = the InternalRel of R;
set CR = the carrier of R;
let x be Element of the carrier of R; :: thesis: Class ((EqRel R),x) = {x}
A1: R is quasi_ordered by Def3;
A2: the InternalRel of R is_antisymmetric_in the carrier of R by ORDERS_2:def 6;

now

let z be set ; :: thesis: ( ( z in Class ((EqRel R),x) implies z in {x} ) & ( z in {x} implies z in Class ((EqRel R),x) ) )

hereby :: thesis: ( z in {x} implies z in Class ((EqRel R),x) )

assume z in Class ((EqRel R),x) ; :: thesis: z in {x}
then [z,x] in EqRel R by EQREL_1:27;
then A3: [z,x] in the InternalRel of R /\ ( the InternalRel of R ~) by A1, Def4;
then A4: [z,x] in the InternalRel of R by XBOOLE_0:def 4;
[z,x] in the InternalRel of R ~ by A3, XBOOLE_0:def 4;
then A5: [x,z] in the InternalRel of R by RELAT_1:def 7;
z in dom the InternalRel of R by A4, RELAT_1:def 4;
then z = x by A2, A4, A5, RELAT_2:def 4;
hence z in {x} by TARSKI:def 1; :: thesis: verum

end;

assume z in {x} ; :: thesis: z in Class ((EqRel R),x)
then z = x by TARSKI:def 1;
hence z in Class ((EqRel R),x) by EQREL_1:28; :: thesis: verum

end;

hence Class ((EqRel R),x) = {x} by TARSKI:2; :: thesis: verum