let R be Ring; Class (EqRel (R,([#] R))) = { the carrier of R}
set E = EqRel (R,([#] R));
thus
Class (EqRel (R,([#] R))) c= { the carrier of R}
XBOOLE_0:def 10 { the carrier of R} c= Class (EqRel (R,([#] R)))proof
let A be
object ;
TARSKI:def 3 ( not A in Class (EqRel (R,([#] R))) or A in { the carrier of R} )
assume
A in Class (EqRel (R,([#] R)))
;
A in { the carrier of R}
then consider x being
object such that A1:
x in the
carrier of
R
and A2:
A = Class (
(EqRel (R,([#] R))),
x)
by EQREL_1:def 3;
reconsider x =
x as
Element of
R by A1;
Class (
(EqRel (R,([#] R))),
x)
= the
carrier of
R
proof
thus
Class (
(EqRel (R,([#] R))),
x)
c= the
carrier of
R
;
XBOOLE_0:def 10 the carrier of R c= Class ((EqRel (R,([#] R))),x)
let a be
object ;
TARSKI:def 3 ( not a in the carrier of R or a in Class ((EqRel (R,([#] R))),x) )
assume
a in the
carrier of
R
;
a in Class ((EqRel (R,([#] R))),x)
then reconsider a =
a as
Element of
R ;
a - x in [#] R
;
then
[a,x] in EqRel (
R,
([#] R))
by Def5;
hence
a in Class (
(EqRel (R,([#] R))),
x)
by EQREL_1:19;
verum
end;
hence
A in { the carrier of R}
by A2, TARSKI:def 1;
verum
end;
let A be object ; TARSKI:def 3 ( not A in { the carrier of R} or A in Class (EqRel (R,([#] R))) )
assume
A in { the carrier of R}
; A in Class (EqRel (R,([#] R)))
then A =
the carrier of R
by TARSKI:def 1
.=
Class ((EqRel (R,([#] R))),(0. R))
by Th7
;
hence
A in Class (EqRel (R,([#] R)))
by EQREL_1:def 3; verum