let G be addGroup; :: thesis: for H being Subgroup of G st G is Abelian addGroup holds
H is Abelian
let H be Subgroup of G; :: thesis: ( G is Abelian addGroup implies H is Abelian )
assume A1: G is Abelian addGroup ; :: thesis: H is Abelian
thus for h1, h2 being Element of H holds h1 + h2 = h2 + h1 :: according to RLVECT_1:def 2 :: thesis: verum
proof
let h1, h2 be Element of H; :: thesis: h1 + h2 = h2 + h1
reconsider g1 = h1, g2 = h2 as Element of G by Th41, STRUCT_0:def 5;
thus h1 + h2 = g1 + g2 by Th43
.= g2 + g1 by A1, Lm2
.= h2 + h1 by Th43 ; :: thesis: verum
end;