theorem Th11: :: GROUP_22:11

for G being Group
for H being Subgroup of G holds
( H is proper iff the carrier of G \ the carrier of H is non empty set )