let X, Y be Subset of CQC-WFF ; :: thesis: for f being FinSequence of [:CQC-WFF ,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 ,Proof_Step_Kinds :]; :: thesis: ( 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 ; :: thesis: f is_a_proof_wrt Y
thus f <> {} by A1, Def5; :: according to CQC_THE1:def 5 :: thesis: for n being Element of NAT st 1 <= n & n <= len f holds
f,n is_a_correct_step_wrt Y
let n be Element of NAT ; :: thesis: ( 1 <= n & n <= len f implies f,n is_a_correct_step_wrt Y )
assume A3: ( 1 <= n & n <= len f ) ; :: thesis: f,n is_a_correct_step_wrt Y
A4: f,n is_a_correct_step_wrt X by A1, A3, Def5;
per cases ( (f . n) `2 = 0 or (f . n) `2 = 1 or (f . n) `2 = 2 or (f . n) `2 = 3 or (f . n) `2 = 4 or (f . n) `2 = 5 or (f . n) `2 = 6 or (f . n) `2 = 7 or (f . n) `2 = 8 or (f . n) `2 = 9 ) by A3, Th45;
:: according to CQC_THE1:def 4
case A5: (f . n) `2 = 0 ; :: thesis: (f . n) `1 in Y
A6: (f . n) `1 in X by A4, A5, Def4;
thus (f . n) `1 in Y by A2, A6; :: thesis: verum
end;
case A7: (f . n) `2 = 1 ; :: thesis: (f . n) `1 = VERUM
thus (f . n) `1 = VERUM by A4, A7, Def4; :: thesis: verum
end;
case A8: (f . n) `2 = 2 ; :: thesis: ex p being Element of CQC-WFF st (f . n) `1 = (('not' p) => p) => p
thus ex p being Element of CQC-WFF st (f . n) `1 = (('not' p) => p) => p by A4, A8, Def4; :: thesis: verum
end;
case A9: (f . n) `2 = 3 ; :: thesis: ex p, q being Element of CQC-WFF st (f . n) `1 = p => (('not' p) => q)
thus ex p, q being Element of CQC-WFF st (f . n) `1 = p => (('not' p) => q) by A4, A9, Def4; :: thesis: verum
end;
case A10: (f . n) `2 = 4 ; :: thesis: ex p, q, r being Element of CQC-WFF st (f . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r)))
thus ex p, q, r being Element of CQC-WFF st (f . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) by A4, A10, Def4; :: thesis: verum
end;
case A11: (f . n) `2 = 5 ; :: thesis: ex p, q being Element of CQC-WFF st (f . n) `1 = (p '&' q) => (q '&' p)
thus ex p, q being Element of CQC-WFF st (f . n) `1 = (p '&' q) => (q '&' p) by A4, A11, Def4; :: thesis: verum
end;
case A12: (f . n) `2 = 6 ; :: thesis: ex p being Element of CQC-WFF ex x being bound_QC-variable st (f . n) `1 = (All x,p) => p
thus ex p being Element of CQC-WFF ex x being bound_QC-variable st (f . n) `1 = (All x,p) => p by A4, A12, Def4; :: thesis: verum
end;
case A13: (f . n) `2 = 7 ; :: thesis: ex i, j being Element of NAT ex p, q being Element of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & p = (f . j) `1 & q = (f . n) `1 & (f . i) `1 = p => q )
thus ex i, j being Element of NAT ex p, q being Element of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & p = (f . j) `1 & q = (f . n) `1 & (f . i) `1 = p => q ) by A4, A13, Def4; :: thesis: verum
end;
case A14: (f . n) `2 = 8 ; :: thesis: ex i being Element of NAT ex p, q being Element of CQC-WFF ex x being bound_QC-variable st
( 1 <= i & i < n & (f . i) `1 = p => q & not x in still_not-bound_in p & (f . n) `1 = p => (All x,q) )
thus ex i being Element of NAT ex p, q being Element of CQC-WFF ex x being bound_QC-variable st
( 1 <= i & i < n & (f . i) `1 = p => q & not x in still_not-bound_in p & (f . n) `1 = p => (All x,q) ) by A4, A14, Def4; :: thesis: verum
end;
case A15: (f . n) `2 = 9 ; :: thesis: ex i being Element of NAT ex x, y being bound_QC-variable ex s being QC-formula st
( 1 <= i & i < n & s . x in CQC-WFF & s . y in CQC-WFF & not x in still_not-bound_in s & s . x = (f . i) `1 & s . y = (f . n) `1 )
thus ex i being Element of NAT ex x, y being bound_QC-variable ex s being QC-formula st
( 1 <= i & i < n & s . x in CQC-WFF & s . y in CQC-WFF & not x in still_not-bound_in s & s . x = (f . i) `1 & s . y = (f . n) `1 ) by A4, A15, Def4; :: thesis: verum
end;
end;