for G being finite SimpleGraph holds order G <= card G