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 ;
A2: the InternalRel of R is_antisymmetric_in the carrier of R by ORDERS_2:def 4;

now :: thesis: for z being object holds
( ( z in Class ((EqRel R),x) implies z in {x} ) & ( z in {x} implies z in Class ((EqRel R),x) ) )

let z be object ; :: 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:19;
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, XTUPLE_0:def 12;
then z = x by A2, A4, A5;
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:20; :: thesis: verum

end;

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