let R be commutative Ring; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum

end;

( 0. R in S implies S ~ R is degenerated )

proof

assume 0. R in S ; :: thesis: S ~ R is degenerated
then A6: 1. (R,S), 0. (R,S) Fr_Eq S ;
1. (S ~ R) = Class ((EqRel S),(1. (R,S))) by Def6
.= Class ((EqRel S),(0. (R,S))) by A6, Th26
.= 0. (S ~ R) by Def6 ;
hence S ~ R is degenerated ; :: thesis: verum

end;

hence ( 0. R in S iff S ~ R is degenerated ) by A1; :: thesis: verum