let L be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: - {(0. L)} = {(0. L)}
A: - {(0. L)} c= {(0. L)}

proof

now :: thesis: for o being object st o in - {(0. L)} holds
o in {(0. L)}

let o be object ; :: thesis: ( o in - {(0. L)} implies o in {(0. L)} )
assume o in - {(0. L)} ; :: thesis: o in {(0. L)}
then consider x being Element of L such that
B: ( o = - x & x in {(0. L)} ) ;
x = 0. L by B, TARSKI:def 1;
hence o in {(0. L)} by B; :: thesis: verum

end;

hence - {(0. L)} c= {(0. L)} ; :: thesis: verum

end;

{(0. L)} c= - {(0. L)}

proof

now :: thesis: for o being object st o in {(0. L)} holds
o in - {(0. L)}

let o be object ; :: thesis: ( o in {(0. L)} implies o in - {(0. L)} )
assume B: o in {(0. L)} ; :: thesis: o in - {(0. L)}
then reconsider x = o as Element of L ;
C: x = 0. L by B, TARSKI:def 1;
- x in - {(0. L)} by B;
hence o in - {(0. L)} by C; :: thesis: verum

end;

hence {(0. L)} c= - {(0. L)} ; :: thesis: verum

end;

hence - {(0. L)} = {(0. L)} by A; :: thesis: verum