theorem Th5: :: INTPRO_2:4

for X being Subset of MC-wff
for f being FinSequence of [:MC-wff,Proof_Step_Kinds_IPC:] st f is_a_proof_wrt_IPC X holds
1 <= len f