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
[z,x] in the
InternalRel of
R /\ (the InternalRel of R ~ )
by A1, Def4;
then A3:
(
[z,x] in the
InternalRel of
R &
[z,x] in the
InternalRel of
R ~ )
by XBOOLE_0:def 4;
then A4:
(
[z,x] in the
InternalRel of
R &
[x,z] in the
InternalRel of
R )
by RELAT_1:def 7;
z in dom the
InternalRel of
R
by A3, RELAT_1:def 4;
then
z = x
by A2, A4, 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),xthen
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