let G be addGroup; :: thesis: for g being Element of G
for H being Subgroup of G
for h being Element of H st h = g holds
- h = - g
let g be Element of G; :: thesis: for H being Subgroup of G
for h being Element of H st h = g holds
- h = - g
let H be Subgroup of G; :: thesis: for h being Element of H st h = g holds
- h = - g
let h be Element of H; :: thesis: ( h = g implies - h = - g )
reconsider g9 = - h as Element of G by Th41, STRUCT_0:def 5;
A1: h + (- h) = 0_ H by Def5;
assume h = g ; :: thesis: - h = - g
then g + g9 = 0_ H by A1, Th43
.= 0_ G by Th44 ;
hence - h = - g by Th11; :: thesis: verum