let R be commutative Ring; for S being non empty multiplicatively-closed Subset of R holds
( 0. R in S iff S ~ R is degenerated )
let S be non empty multiplicatively-closed Subset of R; ( 0. R in S iff S ~ R is degenerated )
A1:
( S ~ R is degenerated implies 0. R in S )
proof
assume
S ~ R is
degenerated
;
0. R in S
then Class (
(EqRel S),
(1. (R,S))) =
0. (S ~ R)
by Def6
.=
Class (
(EqRel S),
(0. (R,S)))
by Def6
;
then
1. (
R,
S),
0. (
R,
S)
Fr_Eq S
by Th26;
then consider s1 being
Element of
R such that A3:
s1 in S
and A4:
((((1. (R,S)) `1) * ((0. (R,S)) `2)) - (((0. (R,S)) `1) * ((1. (R,S)) `2))) * s1 = 0. R
;
thus
0. R in S
by A3, A4;
verum
end;
( 0. R in S implies S ~ R is degenerated )
hence
( 0. R in S iff S ~ R is degenerated )
by A1; verum