let Al be QC-alphabet ; for X, Y being Subset of (CQC-WFF Al)
for f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st f is_a_proof_wrt X & X c= Y holds
f is_a_proof_wrt Y
let X, Y be Subset of (CQC-WFF Al); for f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st f is_a_proof_wrt X & X c= Y holds
f is_a_proof_wrt Y
let f be FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:]; ( f is_a_proof_wrt X & X c= Y implies f is_a_proof_wrt Y )
assume that
A1:
f is_a_proof_wrt X
and
A2:
X c= Y
; f is_a_proof_wrt Y
thus
f <> {}
by A1; CQC_THE1:def 5 for n being Nat st 1 <= n & n <= len f holds
f,n is_a_correct_step_wrt Y
let n be Nat; ( 1 <= n & n <= len f implies f,n is_a_correct_step_wrt Y )
assume A3:
( 1 <= n & n <= len f )
; f,n is_a_correct_step_wrt Y
then A4:
f,n is_a_correct_step_wrt X
by A1;
not not (f . n) `2 = 0 & ... & not (f . n) `2 = 9
by A3, Th19;