theorem :: GROUP_23:13

for G being Group
for n being Nat holds (Seg n) --> G is Group-Family of Seg n ;