let R be Ring; :: thesis: for S being Subring of R
for S1 being Subset of R
for S2 being Subset of S st S1 = S2 holds
- S1 = - S2
let S be Subring of R; :: thesis: for S1 being Subset of R
for S2 being Subset of S st S1 = S2 holds
- S1 = - S2
let S1 be Subset of R; :: thesis: for S2 being Subset of S st S1 = S2 holds
- S1 = - S2
let S2 be Subset of S; :: thesis: ( S1 = S2 implies - S1 = - S2 )
assume AS: S1 = S2 ; :: thesis: - S1 = - S2
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: - S2 c= - S1
let o be object ; :: thesis: ( o in - S1 implies o in - S2 )
assume o in - S1 ; :: thesis: o in - S2
then consider a being Element of R such that
A1: ( - a = o & a in S1 ) ;
reconsider b = a as Element of S by A1, AS;
- b in - S2 by A1, AS;
hence o in - S2 by A1, lemminus; :: thesis: verum
end;
let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in - S2 or o in - S1 )
assume o in - S2 ; :: thesis: o in - S1
then consider a being Element of S such that
A1: ( - a = o & a in S2 ) ;
reconsider b = a as Element of R by A1, AS;
- b in - S1 by A1, AS;
hence o in - S1 by A1, lemminus; :: thesis: verum