theorem :: INTPRO_2:3

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
rng f <> {} by RELAT_1:41;