theorem :: GROUP_1:45

for G being non empty finite 1-sorted holds card G >= 1