let R be commutative Ring; for S being non empty multiplicatively-closed Subset of R holds Frac S = [:([#] R),S:]
let S be non empty multiplicatively-closed Subset of R; Frac S = [:([#] R),S:]
for o being object st o in Frac S holds
o in [:([#] R),S:]
then A3:
Frac S c= [:([#] R),S:]
;
for o being object st o in [:([#] R),S:] holds
o in Frac S
proof
let o be
object ;
( o in [:([#] R),S:] implies o in Frac S )
assume
o in [:([#] R),S:]
;
o in Frac S
then consider o1,
o2 being
object such that A5:
o1 in [#] R
and A6:
o2 in S
and A7:
o = [o1,o2]
by ZFMISC_1:def 2;
consider a,
b being
Element of
R such that A8:
a = o1
and A9:
b = o2
by A5, A6;
o = [a,b]
by A8, A9, A7;
hence
o in Frac S
by A6, A9, Def3;
verum
end;
then
[:([#] R),S:] c= Frac S
;
hence
Frac S = [:([#] R),S:]
by A3, XBOOLE_0:def 10; verum