:: deftheorem Def18 defines index GROUP_2:def 18 :
for G being Group
for H being Subgroup of G st Left_Cosets H is finite holds
for b₃ being Element of NAT holds
( b₃ = index H iff ex B being finite set st
( B = Left_Cosets H & b₃ = card B ) );