let G be addGroup; :: thesis: for A, B being Subset of G st A c= B holds
- A c= - B
let A, B be Subset of G; :: thesis: ( A c= B implies - A c= - B )
assume A1: A c= B ; :: thesis: - A c= - B
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in - A or a in - B )
assume a in - A ; :: thesis: a in - B
then ex g being Element of G st
( a = - g & g in A ) ;
hence a in - B by A1; :: thesis: verum