let R be commutative Ring; :: thesis: 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; :: thesis: Frac S = [:([#] R),S:]
for o being object st o in Frac S holds
o in [:([#] R),S:]

proof

let o be object ; :: thesis: ( o in Frac S implies o in [:([#] R),S:] )
assume o in Frac S ; :: thesis: o in [:([#] R),S:]
then consider a, b being Element of R such that
A2: o = [a,b] and
A3: b in S by Def3;
thus o in [:([#] R),S:] by A2, A3, ZFMISC_1:def 2; :: thesis: verum

end;

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 ; :: thesis: ( o in [:([#] R),S:] implies o in Frac S )
assume o in [:([#] R),S:] ; :: thesis: 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; :: thesis: verum

end;

then [:([#] R),S:] c= Frac S ;
hence Frac S = [:([#] R),S:] by A3, XBOOLE_0:def 10; :: thesis: verum