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
set ;
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
set such that A1:
x in the
carrier of
R
and A2:
A = Class (EqRel R,([#] R)),
x
by EQREL_1:def 5;
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
set ;
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:27;
verum
end;
hence
A in {the carrier of R}
by A2, TARSKI:def 1;
verum
end;
let A be set ; 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 5; verum