let R be non empty Poset; 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; 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 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 ;
( ( z in Class ((EqRel R),x) implies z in {x} ) & ( z in {x} implies z in Class ((EqRel R),x) ) )hereby ( z in {x} implies z in Class ((EqRel R),x) )
assume
z in Class (
(EqRel R),
x)
;
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;
verum
end; assume
z in {x}
;
z in Class ((EqRel R),x)then
z = x
by TARSKI:def 1;
hence
z in Class (
(EqRel R),
x)
by EQREL_1:20;
verum end;
hence
Class ((EqRel R),x) = {x}
by TARSKI:2; verum