:: CQC_THE2 semantic presentation begin theorem Th1: :: CQC_THE2:1 for A being QC-alphabet for p, q, r being Element of CQC-WFF A st p => (q => r) is valid holds (p '&' q) => r is valid proof let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A st p => (q => r) is valid holds (p '&' q) => r is valid let p, q, r be Element of CQC-WFF A; ::_thesis: ( p => (q => r) is valid implies (p '&' q) => r is valid ) A1: (p => (q => r)) => ((p '&' q) => r) in TAUT A by PROCAL_1:32; assume p => (q => r) in TAUT A ; :: according to CQC_THE1:def_10 ::_thesis: (p '&' q) => r is valid hence (p '&' q) => r in TAUT A by A1, CQC_THE1:46; :: according to CQC_THE1:def_10 ::_thesis: verum end; theorem Th2: :: CQC_THE2:2 for A being QC-alphabet for p, q, r being Element of CQC-WFF A st p => (q => r) is valid holds (q '&' p) => r is valid proof let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A st p => (q => r) is valid holds (q '&' p) => r is valid let p, q, r be Element of CQC-WFF A; ::_thesis: ( p => (q => r) is valid implies (q '&' p) => r is valid ) assume p => (q => r) in TAUT A ; :: according to CQC_THE1:def_10 ::_thesis: (q '&' p) => r is valid then p => (q => r) is valid by CQC_THE1:def_10; then (p '&' q) => r is valid by Th1; then A1: (p '&' q) => r in TAUT A by CQC_THE1:def_10; (q '&' p) => (p '&' q) in TAUT A by CQC_THE1:45; hence (q '&' p) => r in TAUT A by A1, LUKASI_1:3; :: according to CQC_THE1:def_10 ::_thesis: verum end; theorem Th3: :: CQC_THE2:3 for A being QC-alphabet for p, q, r being Element of CQC-WFF A st (p '&' q) => r is valid holds p => (q => r) is valid proof let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A st (p '&' q) => r is valid holds p => (q => r) is valid let p, q, r be Element of CQC-WFF A; ::_thesis: ( (p '&' q) => r is valid implies p => (q => r) is valid ) A1: ((p '&' q) => r) => (p => (q => r)) in TAUT A by PROCAL_1:31; assume (p '&' q) => r in TAUT A ; :: according to CQC_THE1:def_10 ::_thesis: p => (q => r) is valid hence p => (q => r) in TAUT A by A1, CQC_THE1:46; :: according to CQC_THE1:def_10 ::_thesis: verum end; theorem Th4: :: CQC_THE2:4 for A being QC-alphabet for p, q, r being Element of CQC-WFF A st (p '&' q) => r is valid holds q => (p => r) is valid proof let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A st (p '&' q) => r is valid holds q => (p => r) is valid let p, q, r be Element of CQC-WFF A; ::_thesis: ( (p '&' q) => r is valid implies q => (p => r) is valid ) A1: (q '&' p) => (p '&' q) in TAUT A by CQC_THE1:45; assume (p '&' q) => r in TAUT A ; :: according to CQC_THE1:def_10 ::_thesis: q => (p => r) is valid then (q '&' p) => r in TAUT A by A1, LUKASI_1:3; then (q '&' p) => r is valid by CQC_THE1:def_10; then q => (p => r) is valid by Th3; hence q => (p => r) in TAUT A by CQC_THE1:def_10; :: according to CQC_THE1:def_10 ::_thesis: verum end; Lm1: for A being QC-alphabet for p, q being Element of CQC-WFF A holds ( (p '&' q) => p is valid & (p '&' q) => q is valid ) proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds ( (p '&' q) => p is valid & (p '&' q) => q is valid ) let p, q be Element of CQC-WFF A; ::_thesis: ( (p '&' q) => p is valid & (p '&' q) => q is valid ) thus ( (p '&' q) => p in TAUT A & (p '&' q) => q in TAUT A ) by PROCAL_1:19, PROCAL_1:21; :: according to CQC_THE1:def_10 ::_thesis: verum end; Lm2: for A being QC-alphabet for p, q being Element of CQC-WFF A st p '&' q is valid holds ( p is valid & q is valid ) proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A st p '&' q is valid holds ( p is valid & q is valid ) let p, q be Element of CQC-WFF A; ::_thesis: ( p '&' q is valid implies ( p is valid & q is valid ) ) assume A1: p '&' q is valid ; ::_thesis: ( p is valid & q is valid ) ( (p '&' q) => p is valid & (p '&' q) => q is valid ) by Lm1; hence ( p is valid & q is valid ) by A1, CQC_THE1:65; ::_thesis: verum end; Lm3: for A being QC-alphabet for p, q, r being Element of CQC-WFF A st p => q is valid & p => r is valid holds p => (q '&' r) is valid proof let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A st p => q is valid & p => r is valid holds p => (q '&' r) is valid let p, q, r be Element of CQC-WFF A; ::_thesis: ( p => q is valid & p => r is valid implies p => (q '&' r) is valid ) assume ( p => q in TAUT A & p => r in TAUT A ) ; :: according to CQC_THE1:def_10 ::_thesis: p => (q '&' r) is valid hence p => (q '&' r) in TAUT A by PROCAL_1:52; :: according to CQC_THE1:def_10 ::_thesis: verum end; Lm4: for A being QC-alphabet for p, q, r, t being Element of CQC-WFF A st p => q is valid & r => t is valid holds (p 'or' r) => (q 'or' t) is valid proof let A be QC-alphabet ; ::_thesis: for p, q, r, t being Element of CQC-WFF A st p => q is valid & r => t is valid holds (p 'or' r) => (q 'or' t) is valid let p, q, r, t be Element of CQC-WFF A; ::_thesis: ( p => q is valid & r => t is valid implies (p 'or' r) => (q 'or' t) is valid ) assume ( p => q in TAUT A & r => t in TAUT A ) ; :: according to CQC_THE1:def_10 ::_thesis: (p 'or' r) => (q 'or' t) is valid hence (p 'or' r) => (q 'or' t) in TAUT A by PROCAL_1:57; :: according to CQC_THE1:def_10 ::_thesis: verum end; Lm5: for A being QC-alphabet for p, q, r, t being Element of CQC-WFF A st p => q is valid & r => t is valid holds (p '&' r) => (q '&' t) is valid proof let A be QC-alphabet ; ::_thesis: for p, q, r, t being Element of CQC-WFF A st p => q is valid & r => t is valid holds (p '&' r) => (q '&' t) is valid let p, q, r, t be Element of CQC-WFF A; ::_thesis: ( p => q is valid & r => t is valid implies (p '&' r) => (q '&' t) is valid ) assume ( p => q in TAUT A & r => t in TAUT A ) ; :: according to CQC_THE1:def_10 ::_thesis: (p '&' r) => (q '&' t) is valid hence (p '&' r) => (q '&' t) in TAUT A by PROCAL_1:56; :: according to CQC_THE1:def_10 ::_thesis: verum end; Lm6: for A being QC-alphabet for p, q being Element of CQC-WFF A holds ( p => (p 'or' q) is valid & p => (q 'or' p) is valid ) proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds ( p => (p 'or' q) is valid & p => (q 'or' p) is valid ) let p, q be Element of CQC-WFF A; ::_thesis: ( p => (p 'or' q) is valid & p => (q 'or' p) is valid ) thus ( p => (p 'or' q) in TAUT A & p => (q 'or' p) in TAUT A ) by PROCAL_1:3, PROCAL_1:4; :: according to CQC_THE1:def_10 ::_thesis: verum end; Lm7: for A being QC-alphabet for p, q, r being Element of CQC-WFF A st p => q is valid & r => q is valid holds (p 'or' r) => q is valid proof let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A st p => q is valid & r => q is valid holds (p 'or' r) => q is valid let p, q, r be Element of CQC-WFF A; ::_thesis: ( p => q is valid & r => q is valid implies (p 'or' r) => q is valid ) assume ( p => q in TAUT A & r => q in TAUT A ) ; :: according to CQC_THE1:def_10 ::_thesis: (p 'or' r) => q is valid hence (p 'or' r) => q in TAUT A by PROCAL_1:53; :: according to CQC_THE1:def_10 ::_thesis: verum end; Lm8: for A being QC-alphabet for p, q being Element of CQC-WFF A st p is valid & q is valid holds p '&' q is valid proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A st p is valid & q is valid holds p '&' q is valid let p, q be Element of CQC-WFF A; ::_thesis: ( p is valid & q is valid implies p '&' q is valid ) assume ( p in TAUT A & q in TAUT A ) ; :: according to CQC_THE1:def_10 ::_thesis: p '&' q is valid hence p '&' q in TAUT A by PROCAL_1:47; :: according to CQC_THE1:def_10 ::_thesis: verum end; Lm9: for A being QC-alphabet for p, q, r being Element of CQC-WFF A st p => q is valid holds (r '&' p) => (r '&' q) is valid proof let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A st p => q is valid holds (r '&' p) => (r '&' q) is valid let p, q, r be Element of CQC-WFF A; ::_thesis: ( p => q is valid implies (r '&' p) => (r '&' q) is valid ) assume p => q in TAUT A ; :: according to CQC_THE1:def_10 ::_thesis: (r '&' p) => (r '&' q) is valid hence (r '&' p) => (r '&' q) in TAUT A by PROCAL_1:50; :: according to CQC_THE1:def_10 ::_thesis: verum end; Lm10: for A being QC-alphabet for p, q, r being Element of CQC-WFF A st p => q is valid holds (p 'or' r) => (q 'or' r) is valid proof let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A st p => q is valid holds (p 'or' r) => (q 'or' r) is valid let p, q, r be Element of CQC-WFF A; ::_thesis: ( p => q is valid implies (p 'or' r) => (q 'or' r) is valid ) assume p => q in TAUT A ; :: according to CQC_THE1:def_10 ::_thesis: (p 'or' r) => (q 'or' r) is valid hence (p 'or' r) => (q 'or' r) in TAUT A by PROCAL_1:48; :: according to CQC_THE1:def_10 ::_thesis: verum end; Lm11: for A being QC-alphabet for p, q being Element of CQC-WFF A holds (p 'or' q) => (('not' p) => q) is valid proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds (p 'or' q) => (('not' p) => q) is valid let p, q be Element of CQC-WFF A; ::_thesis: (p 'or' q) => (('not' p) => q) is valid thus (p 'or' q) => (('not' p) => q) in TAUT A by PROCAL_1:5; :: according to CQC_THE1:def_10 ::_thesis: verum end; Lm12: for A being QC-alphabet for p, q being Element of CQC-WFF A holds (('not' p) => q) => (p 'or' q) is valid proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds (('not' p) => q) => (p 'or' q) is valid let p, q be Element of CQC-WFF A; ::_thesis: (('not' p) => q) => (p 'or' q) is valid ('not' ('not' p)) => p in TAUT A by LUKASI_1:25; then ( (('not' p) => q) => (('not' ('not' p)) 'or' q) in TAUT A & (('not' ('not' p)) 'or' q) => (p 'or' q) in TAUT A ) by PROCAL_1:14, PROCAL_1:48; hence (('not' p) => q) => (p 'or' q) in TAUT A by LUKASI_1:3; :: according to CQC_THE1:def_10 ::_thesis: verum end; Lm13: for A being QC-alphabet for p being Element of CQC-WFF A holds p <=> p is valid proof let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A holds p <=> p is valid let p be Element of CQC-WFF A; ::_thesis: p <=> p is valid (p => p) '&' (p => p) is valid by Lm8; hence p <=> p is valid by QC_LANG2:def_4; ::_thesis: verum end; Lm14: for A being QC-alphabet for p, q being Element of CQC-WFF A holds ( ( p => q is valid & q => p is valid ) iff p <=> q is valid ) proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds ( ( p => q is valid & q => p is valid ) iff p <=> q is valid ) let p, q be Element of CQC-WFF A; ::_thesis: ( ( p => q is valid & q => p is valid ) iff p <=> q is valid ) thus ( p => q is valid & q => p is valid implies p <=> q is valid ) ::_thesis: ( p <=> q is valid implies ( p => q is valid & q => p is valid ) ) proof assume ( p => q is valid & q => p is valid ) ; ::_thesis: p <=> q is valid then (p => q) '&' (q => p) is valid by Lm8; hence p <=> q is valid by QC_LANG2:def_4; ::_thesis: verum end; assume p <=> q is valid ; ::_thesis: ( p => q is valid & q => p is valid ) then (p => q) '&' (q => p) is valid by QC_LANG2:def_4; hence ( p => q is valid & q => p is valid ) by Lm2; ::_thesis: verum end; Lm15: for A being QC-alphabet for p, q being Element of CQC-WFF A st p <=> q is valid holds ( p is valid iff q is valid ) proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A st p <=> q is valid holds ( p is valid iff q is valid ) let p, q be Element of CQC-WFF A; ::_thesis: ( p <=> q is valid implies ( p is valid iff q is valid ) ) assume A1: p <=> q in TAUT A ; :: according to CQC_THE1:def_10 ::_thesis: ( p is valid iff q is valid ) (p <=> q) => (p => q) in TAUT A by PROCAL_1:23; then A2: p => q in TAUT A by A1, CQC_THE1:46; thus ( p is valid implies q is valid ) ::_thesis: ( q is valid implies p is valid ) proof assume p in TAUT A ; :: according to CQC_THE1:def_10 ::_thesis: q is valid hence q in TAUT A by A2, CQC_THE1:46; :: according to CQC_THE1:def_10 ::_thesis: verum end; assume A3: q in TAUT A ; :: according to CQC_THE1:def_10 ::_thesis: p is valid (p <=> q) => (q => p) in TAUT A by PROCAL_1:24; then q => p in TAUT A by A1, CQC_THE1:46; hence p in TAUT A by A3, CQC_THE1:46; :: according to CQC_THE1:def_10 ::_thesis: verum end; Lm16: for A being QC-alphabet for p, q, r, t being Element of CQC-WFF A st p => (q => r) is valid & r => t is valid holds p => (q => t) is valid proof let A be QC-alphabet ; ::_thesis: for p, q, r, t being Element of CQC-WFF A st p => (q => r) is valid & r => t is valid holds p => (q => t) is valid let p, q, r, t be Element of CQC-WFF A; ::_thesis: ( p => (q => r) is valid & r => t is valid implies p => (q => t) is valid ) assume that A1: p => (q => r) is valid and A2: r => t is valid ; ::_thesis: p => (q => t) is valid (p '&' q) => r is valid by A1, Th1; then (p '&' q) => t is valid by A2, LUKASI_1:42; hence p => (q => t) is valid by Th3; ::_thesis: verum end; theorem Th5: :: CQC_THE2:5 for A being QC-alphabet for s being QC-formula of A for y, x being bound_QC-variable of A holds ( y in still_not-bound_in (All (x,s)) iff ( y in still_not-bound_in s & y <> x ) ) proof let A be QC-alphabet ; ::_thesis: for s being QC-formula of A for y, x being bound_QC-variable of A holds ( y in still_not-bound_in (All (x,s)) iff ( y in still_not-bound_in s & y <> x ) ) let s be QC-formula of A; ::_thesis: for y, x being bound_QC-variable of A holds ( y in still_not-bound_in (All (x,s)) iff ( y in still_not-bound_in s & y <> x ) ) let y, x be bound_QC-variable of A; ::_thesis: ( y in still_not-bound_in (All (x,s)) iff ( y in still_not-bound_in s & y <> x ) ) still_not-bound_in (All (x,s)) = (still_not-bound_in s) \ {x} by QC_LANG3:12; hence ( y in still_not-bound_in (All (x,s)) iff ( y in still_not-bound_in s & y <> x ) ) by ZFMISC_1:56; ::_thesis: verum end; theorem Th6: :: CQC_THE2:6 for A being QC-alphabet for s being QC-formula of A for y, x being bound_QC-variable of A holds ( y in still_not-bound_in (Ex (x,s)) iff ( y in still_not-bound_in s & y <> x ) ) proof let A be QC-alphabet ; ::_thesis: for s being QC-formula of A for y, x being bound_QC-variable of A holds ( y in still_not-bound_in (Ex (x,s)) iff ( y in still_not-bound_in s & y <> x ) ) let s be QC-formula of A; ::_thesis: for y, x being bound_QC-variable of A holds ( y in still_not-bound_in (Ex (x,s)) iff ( y in still_not-bound_in s & y <> x ) ) let y, x be bound_QC-variable of A; ::_thesis: ( y in still_not-bound_in (Ex (x,s)) iff ( y in still_not-bound_in s & y <> x ) ) still_not-bound_in (Ex (x,s)) = (still_not-bound_in s) \ {x} by QC_LANG3:19; hence ( y in still_not-bound_in (Ex (x,s)) iff ( y in still_not-bound_in s & y <> x ) ) by ZFMISC_1:56; ::_thesis: verum end; theorem Th7: :: CQC_THE2:7 for A being QC-alphabet for s, h being QC-formula of A for y being bound_QC-variable of A holds ( y in still_not-bound_in (s => h) iff ( y in still_not-bound_in s or y in still_not-bound_in h ) ) proof let A be QC-alphabet ; ::_thesis: for s, h being QC-formula of A for y being bound_QC-variable of A holds ( y in still_not-bound_in (s => h) iff ( y in still_not-bound_in s or y in still_not-bound_in h ) ) let s, h be QC-formula of A; ::_thesis: for y being bound_QC-variable of A holds ( y in still_not-bound_in (s => h) iff ( y in still_not-bound_in s or y in still_not-bound_in h ) ) let y be bound_QC-variable of A; ::_thesis: ( y in still_not-bound_in (s => h) iff ( y in still_not-bound_in s or y in still_not-bound_in h ) ) still_not-bound_in (s => h) = (still_not-bound_in s) \/ (still_not-bound_in h) by QC_LANG3:16; hence ( y in still_not-bound_in (s => h) iff ( y in still_not-bound_in s or y in still_not-bound_in h ) ) by XBOOLE_0:def_3; ::_thesis: verum end; theorem Th8: :: CQC_THE2:8 for A being QC-alphabet for s, h being QC-formula of A for y being bound_QC-variable of A holds ( y in still_not-bound_in (s '&' h) iff ( y in still_not-bound_in s or y in still_not-bound_in h ) ) proof let A be QC-alphabet ; ::_thesis: for s, h being QC-formula of A for y being bound_QC-variable of A holds ( y in still_not-bound_in (s '&' h) iff ( y in still_not-bound_in s or y in still_not-bound_in h ) ) let s, h be QC-formula of A; ::_thesis: for y being bound_QC-variable of A holds ( y in still_not-bound_in (s '&' h) iff ( y in still_not-bound_in s or y in still_not-bound_in h ) ) let y be bound_QC-variable of A; ::_thesis: ( y in still_not-bound_in (s '&' h) iff ( y in still_not-bound_in s or y in still_not-bound_in h ) ) still_not-bound_in (s '&' h) = (still_not-bound_in s) \/ (still_not-bound_in h) by QC_LANG3:10; hence ( y in still_not-bound_in (s '&' h) iff ( y in still_not-bound_in s or y in still_not-bound_in h ) ) by XBOOLE_0:def_3; ::_thesis: verum end; theorem Th9: :: CQC_THE2:9 for A being QC-alphabet for s, h being QC-formula of A for y being bound_QC-variable of A holds ( y in still_not-bound_in (s 'or' h) iff ( y in still_not-bound_in s or y in still_not-bound_in h ) ) proof let A be QC-alphabet ; ::_thesis: for s, h being QC-formula of A for y being bound_QC-variable of A holds ( y in still_not-bound_in (s 'or' h) iff ( y in still_not-bound_in s or y in still_not-bound_in h ) ) let s, h be QC-formula of A; ::_thesis: for y being bound_QC-variable of A holds ( y in still_not-bound_in (s 'or' h) iff ( y in still_not-bound_in s or y in still_not-bound_in h ) ) let y be bound_QC-variable of A; ::_thesis: ( y in still_not-bound_in (s 'or' h) iff ( y in still_not-bound_in s or y in still_not-bound_in h ) ) still_not-bound_in (s 'or' h) = (still_not-bound_in s) \/ (still_not-bound_in h) by QC_LANG3:14; hence ( y in still_not-bound_in (s 'or' h) iff ( y in still_not-bound_in s or y in still_not-bound_in h ) ) by XBOOLE_0:def_3; ::_thesis: verum end; theorem :: CQC_THE2:10 for A being QC-alphabet for s being QC-formula of A for x, y being bound_QC-variable of A holds ( not x in still_not-bound_in (All (x,y,s)) & not y in still_not-bound_in (All (x,y,s)) ) proof let A be QC-alphabet ; ::_thesis: for s being QC-formula of A for x, y being bound_QC-variable of A holds ( not x in still_not-bound_in (All (x,y,s)) & not y in still_not-bound_in (All (x,y,s)) ) let s be QC-formula of A; ::_thesis: for x, y being bound_QC-variable of A holds ( not x in still_not-bound_in (All (x,y,s)) & not y in still_not-bound_in (All (x,y,s)) ) let x, y be bound_QC-variable of A; ::_thesis: ( not x in still_not-bound_in (All (x,y,s)) & not y in still_not-bound_in (All (x,y,s)) ) not y in still_not-bound_in (All (y,s)) by Th5; then A1: not y in still_not-bound_in (All (x,(All (y,s)))) by Th5; not x in still_not-bound_in (All (x,(All (y,s)))) by Th5; hence ( not x in still_not-bound_in (All (x,y,s)) & not y in still_not-bound_in (All (x,y,s)) ) by A1, QC_LANG2:14; ::_thesis: verum end; theorem :: CQC_THE2:11 for A being QC-alphabet for s being QC-formula of A for x, y being bound_QC-variable of A holds ( not x in still_not-bound_in (Ex (x,y,s)) & not y in still_not-bound_in (Ex (x,y,s)) ) proof let A be QC-alphabet ; ::_thesis: for s being QC-formula of A for x, y being bound_QC-variable of A holds ( not x in still_not-bound_in (Ex (x,y,s)) & not y in still_not-bound_in (Ex (x,y,s)) ) let s be QC-formula of A; ::_thesis: for x, y being bound_QC-variable of A holds ( not x in still_not-bound_in (Ex (x,y,s)) & not y in still_not-bound_in (Ex (x,y,s)) ) let x, y be bound_QC-variable of A; ::_thesis: ( not x in still_not-bound_in (Ex (x,y,s)) & not y in still_not-bound_in (Ex (x,y,s)) ) not y in still_not-bound_in (Ex (y,s)) by Th6; then A1: not y in still_not-bound_in (Ex (x,(Ex (y,s)))) by Th6; not x in still_not-bound_in (Ex (x,(Ex (y,s)))) by Th6; hence ( not x in still_not-bound_in (Ex (x,y,s)) & not y in still_not-bound_in (Ex (x,y,s)) ) by A1, QC_LANG2:14; ::_thesis: verum end; theorem Th12: :: CQC_THE2:12 for A being QC-alphabet for s, h being QC-formula of A for x being bound_QC-variable of A holds (s => h) . x = (s . x) => (h . x) proof let A be QC-alphabet ; ::_thesis: for s, h being QC-formula of A for x being bound_QC-variable of A holds (s => h) . x = (s . x) => (h . x) let s, h be QC-formula of A; ::_thesis: for x being bound_QC-variable of A holds (s => h) . x = (s . x) => (h . x) let x be bound_QC-variable of A; ::_thesis: (s => h) . x = (s . x) => (h . x) s => h = 'not' (s '&' ('not' h)) by QC_LANG2:def_2; hence (s => h) . x = 'not' ((s '&' ('not' h)) . x) by CQC_LANG:19 .= 'not' ((s . x) '&' (('not' h) . x)) by CQC_LANG:21 .= 'not' ((s . x) '&' ('not' (h . x))) by CQC_LANG:19 .= (s . x) => (h . x) by QC_LANG2:def_2 ; ::_thesis: verum end; theorem :: CQC_THE2:13 for A being QC-alphabet for s, h being QC-formula of A for x being bound_QC-variable of A holds (s 'or' h) . x = (s . x) 'or' (h . x) proof let A be QC-alphabet ; ::_thesis: for s, h being QC-formula of A for x being bound_QC-variable of A holds (s 'or' h) . x = (s . x) 'or' (h . x) let s, h be QC-formula of A; ::_thesis: for x being bound_QC-variable of A holds (s 'or' h) . x = (s . x) 'or' (h . x) let x be bound_QC-variable of A; ::_thesis: (s 'or' h) . x = (s . x) 'or' (h . x) thus (s 'or' h) . x = ('not' (('not' s) '&' ('not' h))) . x by QC_LANG2:def_3 .= 'not' ((('not' s) '&' ('not' h)) . x) by CQC_LANG:19 .= 'not' ((('not' s) . x) '&' (('not' h) . x)) by CQC_LANG:21 .= 'not' (('not' (s . x)) '&' (('not' h) . x)) by CQC_LANG:19 .= 'not' (('not' (s . x)) '&' ('not' (h . x))) by CQC_LANG:19 .= (s . x) 'or' (h . x) by QC_LANG2:def_3 ; ::_thesis: verum end; theorem :: CQC_THE2:14 for A being QC-alphabet for p being Element of CQC-WFF A for x, y being bound_QC-variable of A st x <> y holds (Ex (x,p)) . y = Ex (x,(p . y)) proof let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A for x, y being bound_QC-variable of A st x <> y holds (Ex (x,p)) . y = Ex (x,(p . y)) let p be Element of CQC-WFF A; ::_thesis: for x, y being bound_QC-variable of A st x <> y holds (Ex (x,p)) . y = Ex (x,(p . y)) let x, y be bound_QC-variable of A; ::_thesis: ( x <> y implies (Ex (x,p)) . y = Ex (x,(p . y)) ) assume A1: x <> y ; ::_thesis: (Ex (x,p)) . y = Ex (x,(p . y)) thus (Ex (x,p)) . y = ('not' (All (x,('not' p)))) . y by QC_LANG2:def_5 .= 'not' ((All (x,('not' p))) . y) by CQC_LANG:19 .= 'not' (All (x,(('not' p) . y))) by A1, CQC_LANG:25 .= 'not' (All (x,('not' (p . y)))) by CQC_LANG:19 .= Ex (x,(p . y)) by QC_LANG2:def_5 ; ::_thesis: verum end; theorem Th15: :: CQC_THE2:15 for A being QC-alphabet for p being Element of CQC-WFF A for x being bound_QC-variable of A holds p => (Ex (x,p)) is valid proof let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A for x being bound_QC-variable of A holds p => (Ex (x,p)) is valid let p be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A holds p => (Ex (x,p)) is valid let x be bound_QC-variable of A; ::_thesis: p => (Ex (x,p)) is valid (All (x,('not' p))) => ('not' p) is valid by CQC_THE1:66; then ('not' ('not' p)) => ('not' (All (x,('not' p)))) is valid by LUKASI_1:52; then A1: ('not' ('not' p)) => (Ex (x,p)) is valid by QC_LANG2:def_5; (('not' ('not' p)) => (Ex (x,p))) => (p => (Ex (x,p))) is valid ; hence p => (Ex (x,p)) is valid by A1, CQC_THE1:65; ::_thesis: verum end; theorem Th16: :: CQC_THE2:16 for A being QC-alphabet for p being Element of CQC-WFF A for x being bound_QC-variable of A st p is valid holds Ex (x,p) is valid proof let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A for x being bound_QC-variable of A st p is valid holds Ex (x,p) is valid let p be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A st p is valid holds Ex (x,p) is valid let x be bound_QC-variable of A; ::_thesis: ( p is valid implies Ex (x,p) is valid ) assume A1: p is valid ; ::_thesis: Ex (x,p) is valid p => (Ex (x,p)) is valid by Th15; hence Ex (x,p) is valid by A1, CQC_THE1:65; ::_thesis: verum end; theorem :: CQC_THE2:17 for A being QC-alphabet for p being Element of CQC-WFF A for x being bound_QC-variable of A holds (All (x,p)) => (Ex (x,p)) is valid proof let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A for x being bound_QC-variable of A holds (All (x,p)) => (Ex (x,p)) is valid let p be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A holds (All (x,p)) => (Ex (x,p)) is valid let x be bound_QC-variable of A; ::_thesis: (All (x,p)) => (Ex (x,p)) is valid ( (All (x,p)) => p is valid & p => (Ex (x,p)) is valid ) by Th15, CQC_THE1:66; hence (All (x,p)) => (Ex (x,p)) is valid by LUKASI_1:42; ::_thesis: verum end; theorem :: CQC_THE2:18 for A being QC-alphabet for p being Element of CQC-WFF A for x, y being bound_QC-variable of A holds (All (x,p)) => (Ex (y,p)) is valid proof let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A for x, y being bound_QC-variable of A holds (All (x,p)) => (Ex (y,p)) is valid let p be Element of CQC-WFF A; ::_thesis: for x, y being bound_QC-variable of A holds (All (x,p)) => (Ex (y,p)) is valid let x, y be bound_QC-variable of A; ::_thesis: (All (x,p)) => (Ex (y,p)) is valid ( (All (x,p)) => p is valid & p => (Ex (y,p)) is valid ) by Th15, CQC_THE1:66; hence (All (x,p)) => (Ex (y,p)) is valid by LUKASI_1:42; ::_thesis: verum end; theorem Th19: :: CQC_THE2:19 for A being QC-alphabet for p, q being Element of CQC-WFF A for x being bound_QC-variable of A st p => q is valid & not x in still_not-bound_in q holds (Ex (x,p)) => q is valid proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A for x being bound_QC-variable of A st p => q is valid & not x in still_not-bound_in q holds (Ex (x,p)) => q is valid let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A st p => q is valid & not x in still_not-bound_in q holds (Ex (x,p)) => q is valid let x be bound_QC-variable of A; ::_thesis: ( p => q is valid & not x in still_not-bound_in q implies (Ex (x,p)) => q is valid ) assume ( p => q is valid & not x in still_not-bound_in q ) ; ::_thesis: (Ex (x,p)) => q is valid then ( ('not' q) => ('not' p) is valid & not x in still_not-bound_in ('not' q) ) by LUKASI_1:52, QC_LANG3:7; then ('not' q) => (All (x,('not' p))) is valid by CQC_THE1:67; then ('not' (All (x,('not' p)))) => ('not' ('not' q)) is valid by LUKASI_1:52; then (Ex (x,p)) => ('not' ('not' q)) is valid by QC_LANG2:def_5; hence (Ex (x,p)) => q is valid by LUKASI_1:55; ::_thesis: verum end; theorem Th20: :: CQC_THE2:20 for A being QC-alphabet for p being Element of CQC-WFF A for x being bound_QC-variable of A st not x in still_not-bound_in p holds (Ex (x,p)) => p is valid proof let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A for x being bound_QC-variable of A st not x in still_not-bound_in p holds (Ex (x,p)) => p is valid let p be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A st not x in still_not-bound_in p holds (Ex (x,p)) => p is valid let x be bound_QC-variable of A; ::_thesis: ( not x in still_not-bound_in p implies (Ex (x,p)) => p is valid ) A1: p => p is valid ; assume not x in still_not-bound_in p ; ::_thesis: (Ex (x,p)) => p is valid hence (Ex (x,p)) => p is valid by A1, Th19; ::_thesis: verum end; theorem :: CQC_THE2:21 for A being QC-alphabet for p being Element of CQC-WFF A for x being bound_QC-variable of A st not x in still_not-bound_in p & Ex (x,p) is valid holds p is valid proof let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A for x being bound_QC-variable of A st not x in still_not-bound_in p & Ex (x,p) is valid holds p is valid let p be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A st not x in still_not-bound_in p & Ex (x,p) is valid holds p is valid let x be bound_QC-variable of A; ::_thesis: ( not x in still_not-bound_in p & Ex (x,p) is valid implies p is valid ) assume that A1: not x in still_not-bound_in p and A2: Ex (x,p) is valid ; ::_thesis: p is valid (Ex (x,p)) => p is valid by A1, Th20; hence p is valid by A2, CQC_THE1:65; ::_thesis: verum end; theorem Th22: :: CQC_THE2:22 for A being QC-alphabet for p, q being Element of CQC-WFF A for h being QC-formula of A for x, y being bound_QC-variable of A st p = h . x & q = h . y & not y in still_not-bound_in h holds p => (Ex (y,q)) is valid proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A for h being QC-formula of A for x, y being bound_QC-variable of A st p = h . x & q = h . y & not y in still_not-bound_in h holds p => (Ex (y,q)) is valid let p, q be Element of CQC-WFF A; ::_thesis: for h being QC-formula of A for x, y being bound_QC-variable of A st p = h . x & q = h . y & not y in still_not-bound_in h holds p => (Ex (y,q)) is valid let h be QC-formula of A; ::_thesis: for x, y being bound_QC-variable of A st p = h . x & q = h . y & not y in still_not-bound_in h holds p => (Ex (y,q)) is valid let x, y be bound_QC-variable of A; ::_thesis: ( p = h . x & q = h . y & not y in still_not-bound_in h implies p => (Ex (y,q)) is valid ) assume that A1: p = h . x and A2: q = h . y and A3: not y in still_not-bound_in h ; ::_thesis: p => (Ex (y,q)) is valid A4: (h => (Ex (y,q))) . x = (h . x) => ((Ex (y,q)) . x) by Th12 .= p => (Ex (y,q)) by A1, CQC_LANG:27 ; not y in still_not-bound_in (Ex (y,q)) by Th6; then A5: not y in still_not-bound_in (h => (Ex (y,q))) by A3, Th7; A6: q => (Ex (y,q)) is valid by Th15; (h => (Ex (y,q))) . y = (h . y) => ((Ex (y,q)) . y) by Th12 .= q => (Ex (y,q)) by A2, CQC_LANG:27 ; hence p => (Ex (y,q)) is valid by A6, A4, A5, CQC_THE1:68; ::_thesis: verum end; theorem Th23: :: CQC_THE2:23 for A being QC-alphabet for p being Element of CQC-WFF A for x being bound_QC-variable of A st p is valid holds All (x,p) is valid proof let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A for x being bound_QC-variable of A st p is valid holds All (x,p) is valid let p be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A st p is valid holds All (x,p) is valid let x be bound_QC-variable of A; ::_thesis: ( p is valid implies All (x,p) is valid ) A1: p => (((All (x,p)) => (All (x,p))) => p) is valid ; not x in still_not-bound_in (All (x,p)) by Th5; then A2: not x in still_not-bound_in ((All (x,p)) => (All (x,p))) by Th7; assume p is valid ; ::_thesis: All (x,p) is valid then ((All (x,p)) => (All (x,p))) => p is valid by A1, CQC_THE1:65; then ((All (x,p)) => (All (x,p))) => (All (x,p)) is valid by A2, CQC_THE1:67; hence All (x,p) is valid by CQC_THE1:65; ::_thesis: verum end; theorem Th24: :: CQC_THE2:24 for A being QC-alphabet for p being Element of CQC-WFF A for x being bound_QC-variable of A st not x in still_not-bound_in p holds p => (All (x,p)) is valid proof let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A for x being bound_QC-variable of A st not x in still_not-bound_in p holds p => (All (x,p)) is valid let p be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A st not x in still_not-bound_in p holds p => (All (x,p)) is valid let x be bound_QC-variable of A; ::_thesis: ( not x in still_not-bound_in p implies p => (All (x,p)) is valid ) A1: p => p is valid ; assume not x in still_not-bound_in p ; ::_thesis: p => (All (x,p)) is valid hence p => (All (x,p)) is valid by A1, CQC_THE1:67; ::_thesis: verum end; theorem Th25: :: CQC_THE2:25 for A being QC-alphabet for p, q being Element of CQC-WFF A for h being QC-formula of A for x, y being bound_QC-variable of A st p = h . x & q = h . y & not x in still_not-bound_in h holds (All (x,p)) => q is valid proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A for h being QC-formula of A for x, y being bound_QC-variable of A st p = h . x & q = h . y & not x in still_not-bound_in h holds (All (x,p)) => q is valid let p, q be Element of CQC-WFF A; ::_thesis: for h being QC-formula of A for x, y being bound_QC-variable of A st p = h . x & q = h . y & not x in still_not-bound_in h holds (All (x,p)) => q is valid let h be QC-formula of A; ::_thesis: for x, y being bound_QC-variable of A st p = h . x & q = h . y & not x in still_not-bound_in h holds (All (x,p)) => q is valid let x, y be bound_QC-variable of A; ::_thesis: ( p = h . x & q = h . y & not x in still_not-bound_in h implies (All (x,p)) => q is valid ) assume that A1: p = h . x and A2: q = h . y and A3: not x in still_not-bound_in h ; ::_thesis: (All (x,p)) => q is valid A4: ((All (x,p)) => h) . y = ((All (x,p)) . y) => q by A2, Th12 .= (All (x,p)) => q by CQC_LANG:27 ; not x in still_not-bound_in (All (x,p)) by Th5; then A5: ( (All (x,p)) => p is valid & not x in still_not-bound_in ((All (x,p)) => h) ) by A3, Th7, CQC_THE1:66; ((All (x,p)) => h) . x = ((All (x,p)) . x) => p by A1, Th12 .= (All (x,p)) => p by CQC_LANG:27 ; hence (All (x,p)) => q is valid by A4, A5, CQC_THE1:68; ::_thesis: verum end; theorem :: CQC_THE2:26 for A being QC-alphabet for p being Element of CQC-WFF A for y, x being bound_QC-variable of A st not y in still_not-bound_in p holds (All (x,p)) => (All (y,p)) is valid proof let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A for y, x being bound_QC-variable of A st not y in still_not-bound_in p holds (All (x,p)) => (All (y,p)) is valid let p be Element of CQC-WFF A; ::_thesis: for y, x being bound_QC-variable of A st not y in still_not-bound_in p holds (All (x,p)) => (All (y,p)) is valid let y, x be bound_QC-variable of A; ::_thesis: ( not y in still_not-bound_in p implies (All (x,p)) => (All (y,p)) is valid ) assume not y in still_not-bound_in p ; ::_thesis: (All (x,p)) => (All (y,p)) is valid then ( (All (x,p)) => p is valid & not y in still_not-bound_in (All (x,p)) ) by Th5, CQC_THE1:66; hence (All (x,p)) => (All (y,p)) is valid by CQC_THE1:67; ::_thesis: verum end; theorem :: CQC_THE2:27 for A being QC-alphabet for p, q being Element of CQC-WFF A for h being QC-formula of A for x, y being bound_QC-variable of A st p = h . x & q = h . y & not x in still_not-bound_in h & not y in still_not-bound_in p holds (All (x,p)) => (All (y,q)) is valid proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A for h being QC-formula of A for x, y being bound_QC-variable of A st p = h . x & q = h . y & not x in still_not-bound_in h & not y in still_not-bound_in p holds (All (x,p)) => (All (y,q)) is valid let p, q be Element of CQC-WFF A; ::_thesis: for h being QC-formula of A for x, y being bound_QC-variable of A st p = h . x & q = h . y & not x in still_not-bound_in h & not y in still_not-bound_in p holds (All (x,p)) => (All (y,q)) is valid let h be QC-formula of A; ::_thesis: for x, y being bound_QC-variable of A st p = h . x & q = h . y & not x in still_not-bound_in h & not y in still_not-bound_in p holds (All (x,p)) => (All (y,q)) is valid let x, y be bound_QC-variable of A; ::_thesis: ( p = h . x & q = h . y & not x in still_not-bound_in h & not y in still_not-bound_in p implies (All (x,p)) => (All (y,q)) is valid ) assume ( p = h . x & q = h . y & not x in still_not-bound_in h & not y in still_not-bound_in p ) ; ::_thesis: (All (x,p)) => (All (y,q)) is valid then ( not y in still_not-bound_in (All (x,p)) & (All (x,p)) => q is valid ) by Th5, Th25; hence (All (x,p)) => (All (y,q)) is valid by CQC_THE1:67; ::_thesis: verum end; theorem :: CQC_THE2:28 for A being QC-alphabet for p being Element of CQC-WFF A for x, y being bound_QC-variable of A st not x in still_not-bound_in p holds (Ex (x,p)) => (Ex (y,p)) is valid proof let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A for x, y being bound_QC-variable of A st not x in still_not-bound_in p holds (Ex (x,p)) => (Ex (y,p)) is valid let p be Element of CQC-WFF A; ::_thesis: for x, y being bound_QC-variable of A st not x in still_not-bound_in p holds (Ex (x,p)) => (Ex (y,p)) is valid let x, y be bound_QC-variable of A; ::_thesis: ( not x in still_not-bound_in p implies (Ex (x,p)) => (Ex (y,p)) is valid ) assume not x in still_not-bound_in p ; ::_thesis: (Ex (x,p)) => (Ex (y,p)) is valid then A1: not x in still_not-bound_in (Ex (y,p)) by Th6; p => (Ex (y,p)) is valid by Th15; hence (Ex (x,p)) => (Ex (y,p)) is valid by A1, Th19; ::_thesis: verum end; theorem :: CQC_THE2:29 for A being QC-alphabet for p, q being Element of CQC-WFF A for h being QC-formula of A for x, y being bound_QC-variable of A st p = h . x & q = h . y & not x in still_not-bound_in q & not y in still_not-bound_in h holds (Ex (x,p)) => (Ex (y,q)) is valid proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A for h being QC-formula of A for x, y being bound_QC-variable of A st p = h . x & q = h . y & not x in still_not-bound_in q & not y in still_not-bound_in h holds (Ex (x,p)) => (Ex (y,q)) is valid let p, q be Element of CQC-WFF A; ::_thesis: for h being QC-formula of A for x, y being bound_QC-variable of A st p = h . x & q = h . y & not x in still_not-bound_in q & not y in still_not-bound_in h holds (Ex (x,p)) => (Ex (y,q)) is valid let h be QC-formula of A; ::_thesis: for x, y being bound_QC-variable of A st p = h . x & q = h . y & not x in still_not-bound_in q & not y in still_not-bound_in h holds (Ex (x,p)) => (Ex (y,q)) is valid let x, y be bound_QC-variable of A; ::_thesis: ( p = h . x & q = h . y & not x in still_not-bound_in q & not y in still_not-bound_in h implies (Ex (x,p)) => (Ex (y,q)) is valid ) assume ( p = h . x & q = h . y & not x in still_not-bound_in q & not y in still_not-bound_in h ) ; ::_thesis: (Ex (x,p)) => (Ex (y,q)) is valid then ( not x in still_not-bound_in (Ex (y,q)) & p => (Ex (y,q)) is valid ) by Th6, Th22; hence (Ex (x,p)) => (Ex (y,q)) is valid by Th19; ::_thesis: verum end; theorem Th30: :: CQC_THE2:30 for A being QC-alphabet for p, q being Element of CQC-WFF A for x being bound_QC-variable of A holds (All (x,(p => q))) => ((All (x,p)) => (All (x,q))) is valid proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A for x being bound_QC-variable of A holds (All (x,(p => q))) => ((All (x,p)) => (All (x,q))) is valid let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A holds (All (x,(p => q))) => ((All (x,p)) => (All (x,q))) is valid let x be bound_QC-variable of A; ::_thesis: (All (x,(p => q))) => ((All (x,p)) => (All (x,q))) is valid (All (x,(p => q))) => (p => q) is valid by CQC_THE1:66; then A1: p => ((All (x,(p => q))) => q) is valid by LUKASI_1:44; (All (x,p)) => p is valid by CQC_THE1:66; then (All (x,p)) => ((All (x,(p => q))) => q) is valid by A1, LUKASI_1:42; then A2: ((All (x,(p => q))) '&' (All (x,p))) => q is valid by Th2; ( not x in still_not-bound_in (All (x,(p => q))) & not x in still_not-bound_in (All (x,p)) ) by Th5; then not x in still_not-bound_in ((All (x,(p => q))) '&' (All (x,p))) by Th8; then ((All (x,(p => q))) '&' (All (x,p))) => (All (x,q)) is valid by A2, CQC_THE1:67; hence (All (x,(p => q))) => ((All (x,p)) => (All (x,q))) is valid by Th3; ::_thesis: verum end; theorem Th31: :: CQC_THE2:31 for A being QC-alphabet for p, q being Element of CQC-WFF A for x being bound_QC-variable of A st All (x,(p => q)) is valid holds (All (x,p)) => (All (x,q)) is valid proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A for x being bound_QC-variable of A st All (x,(p => q)) is valid holds (All (x,p)) => (All (x,q)) is valid let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A st All (x,(p => q)) is valid holds (All (x,p)) => (All (x,q)) is valid let x be bound_QC-variable of A; ::_thesis: ( All (x,(p => q)) is valid implies (All (x,p)) => (All (x,q)) is valid ) assume A1: All (x,(p => q)) is valid ; ::_thesis: (All (x,p)) => (All (x,q)) is valid (All (x,(p => q))) => ((All (x,p)) => (All (x,q))) is valid by Th30; hence (All (x,p)) => (All (x,q)) is valid by A1, CQC_THE1:65; ::_thesis: verum end; theorem Th32: :: CQC_THE2:32 for A being QC-alphabet for p, q being Element of CQC-WFF A for x being bound_QC-variable of A holds (All (x,(p <=> q))) => ((All (x,p)) <=> (All (x,q))) is valid proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A for x being bound_QC-variable of A holds (All (x,(p <=> q))) => ((All (x,p)) <=> (All (x,q))) is valid let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A holds (All (x,(p <=> q))) => ((All (x,p)) <=> (All (x,q))) is valid let x be bound_QC-variable of A; ::_thesis: (All (x,(p <=> q))) => ((All (x,p)) <=> (All (x,q))) is valid A1: (All (x,((p => q) '&' (q => p)))) => ((p => q) '&' (q => p)) is valid by CQC_THE1:66; (p <=> q) => (p <=> q) is valid ; then (p <=> q) => ((p => q) '&' (q => p)) is valid by QC_LANG2:def_4; then All (x,((p <=> q) => ((p => q) '&' (q => p)))) is valid by Th23; then A2: (All (x,(p <=> q))) => (All (x,((p => q) '&' (q => p)))) is valid by Th31; ( (All (x,(p => q))) => ((All (x,p)) => (All (x,q))) is valid & (All (x,(q => p))) => ((All (x,q)) => (All (x,p))) is valid ) by Th30; then ((All (x,(p => q))) '&' (All (x,(q => p)))) => (((All (x,p)) => (All (x,q))) '&' ((All (x,q)) => (All (x,p)))) is valid by Lm5; then A3: ((All (x,(p => q))) '&' (All (x,(q => p)))) => ((All (x,p)) <=> (All (x,q))) is valid by QC_LANG2:def_4; A4: not x in still_not-bound_in (All (x,((p => q) '&' (q => p)))) by Th5; ((p => q) '&' (q => p)) => (q => p) is valid by Lm1; then (All (x,((p => q) '&' (q => p)))) => (q => p) is valid by A1, LUKASI_1:42; then A5: (All (x,((p => q) '&' (q => p)))) => (All (x,(q => p))) is valid by A4, CQC_THE1:67; ((p => q) '&' (q => p)) => (p => q) is valid by Lm1; then (All (x,((p => q) '&' (q => p)))) => (p => q) is valid by A1, LUKASI_1:42; then (All (x,((p => q) '&' (q => p)))) => (All (x,(p => q))) is valid by A4, CQC_THE1:67; then (All (x,((p => q) '&' (q => p)))) => ((All (x,(p => q))) '&' (All (x,(q => p)))) is valid by A5, Lm3; then (All (x,((p => q) '&' (q => p)))) => ((All (x,p)) <=> (All (x,q))) is valid by A3, LUKASI_1:42; hence (All (x,(p <=> q))) => ((All (x,p)) <=> (All (x,q))) is valid by A2, LUKASI_1:42; ::_thesis: verum end; theorem :: CQC_THE2:33 for A being QC-alphabet for p, q being Element of CQC-WFF A for x being bound_QC-variable of A st All (x,(p <=> q)) is valid holds (All (x,p)) <=> (All (x,q)) is valid proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A for x being bound_QC-variable of A st All (x,(p <=> q)) is valid holds (All (x,p)) <=> (All (x,q)) is valid let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A st All (x,(p <=> q)) is valid holds (All (x,p)) <=> (All (x,q)) is valid let x be bound_QC-variable of A; ::_thesis: ( All (x,(p <=> q)) is valid implies (All (x,p)) <=> (All (x,q)) is valid ) assume A1: All (x,(p <=> q)) is valid ; ::_thesis: (All (x,p)) <=> (All (x,q)) is valid (All (x,(p <=> q))) => ((All (x,p)) <=> (All (x,q))) is valid by Th32; hence (All (x,p)) <=> (All (x,q)) is valid by A1, CQC_THE1:65; ::_thesis: verum end; theorem Th34: :: CQC_THE2:34 for A being QC-alphabet for p, q being Element of CQC-WFF A for x being bound_QC-variable of A holds (All (x,(p => q))) => ((Ex (x,p)) => (Ex (x,q))) is valid proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A for x being bound_QC-variable of A holds (All (x,(p => q))) => ((Ex (x,p)) => (Ex (x,q))) is valid let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A holds (All (x,(p => q))) => ((Ex (x,p)) => (Ex (x,q))) is valid let x be bound_QC-variable of A; ::_thesis: (All (x,(p => q))) => ((Ex (x,p)) => (Ex (x,q))) is valid (All (x,(p => q))) => (p => q) is valid by CQC_THE1:66; then A1: (p '&' (All (x,(p => q)))) => q is valid by Th2; q => (Ex (x,q)) is valid by Th15; then (p '&' (All (x,(p => q)))) => (Ex (x,q)) is valid by A1, LUKASI_1:42; then A2: p => ((All (x,(p => q))) => (Ex (x,q))) is valid by Th3; ( not x in still_not-bound_in (All (x,(p => q))) & not x in still_not-bound_in (Ex (x,q)) ) by Th5, Th6; then not x in still_not-bound_in ((All (x,(p => q))) => (Ex (x,q))) by Th7; then (Ex (x,p)) => ((All (x,(p => q))) => (Ex (x,q))) is valid by A2, Th19; hence (All (x,(p => q))) => ((Ex (x,p)) => (Ex (x,q))) is valid by LUKASI_1:44; ::_thesis: verum end; theorem Th35: :: CQC_THE2:35 for A being QC-alphabet for p, q being Element of CQC-WFF A for x being bound_QC-variable of A st All (x,(p => q)) is valid holds (Ex (x,p)) => (Ex (x,q)) is valid proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A for x being bound_QC-variable of A st All (x,(p => q)) is valid holds (Ex (x,p)) => (Ex (x,q)) is valid let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A st All (x,(p => q)) is valid holds (Ex (x,p)) => (Ex (x,q)) is valid let x be bound_QC-variable of A; ::_thesis: ( All (x,(p => q)) is valid implies (Ex (x,p)) => (Ex (x,q)) is valid ) assume A1: All (x,(p => q)) is valid ; ::_thesis: (Ex (x,p)) => (Ex (x,q)) is valid (All (x,(p => q))) => ((Ex (x,p)) => (Ex (x,q))) is valid by Th34; hence (Ex (x,p)) => (Ex (x,q)) is valid by A1, CQC_THE1:65; ::_thesis: verum end; theorem Th36: :: CQC_THE2:36 for A being QC-alphabet for p, q being Element of CQC-WFF A for x being bound_QC-variable of A holds ( (All (x,(p '&' q))) => ((All (x,p)) '&' (All (x,q))) is valid & ((All (x,p)) '&' (All (x,q))) => (All (x,(p '&' q))) is valid ) proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A for x being bound_QC-variable of A holds ( (All (x,(p '&' q))) => ((All (x,p)) '&' (All (x,q))) is valid & ((All (x,p)) '&' (All (x,q))) => (All (x,(p '&' q))) is valid ) let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A holds ( (All (x,(p '&' q))) => ((All (x,p)) '&' (All (x,q))) is valid & ((All (x,p)) '&' (All (x,q))) => (All (x,(p '&' q))) is valid ) let x be bound_QC-variable of A; ::_thesis: ( (All (x,(p '&' q))) => ((All (x,p)) '&' (All (x,q))) is valid & ((All (x,p)) '&' (All (x,q))) => (All (x,(p '&' q))) is valid ) ( (All (x,p)) => p is valid & (All (x,q)) => q is valid ) by CQC_THE1:66; then A1: ((All (x,p)) '&' (All (x,q))) => (p '&' q) is valid by Lm5; ( All (x,((p '&' q) => q)) is valid & (All (x,((p '&' q) => q))) => ((All (x,(p '&' q))) => (All (x,q))) is valid ) by Lm1, Th23, Th30; then A2: (All (x,(p '&' q))) => (All (x,q)) is valid by CQC_THE1:65; ( All (x,((p '&' q) => p)) is valid & (All (x,((p '&' q) => p))) => ((All (x,(p '&' q))) => (All (x,p))) is valid ) by Lm1, Th23, Th30; then (All (x,(p '&' q))) => (All (x,p)) is valid by CQC_THE1:65; hence (All (x,(p '&' q))) => ((All (x,p)) '&' (All (x,q))) is valid by A2, Lm3; ::_thesis: ((All (x,p)) '&' (All (x,q))) => (All (x,(p '&' q))) is valid ( not x in still_not-bound_in (All (x,p)) & not x in still_not-bound_in (All (x,q)) ) by Th5; then not x in still_not-bound_in ((All (x,p)) '&' (All (x,q))) by Th8; hence ((All (x,p)) '&' (All (x,q))) => (All (x,(p '&' q))) is valid by A1, CQC_THE1:67; ::_thesis: verum end; theorem Th37: :: CQC_THE2:37 for A being QC-alphabet for p, q being Element of CQC-WFF A for x being bound_QC-variable of A holds (All (x,(p '&' q))) <=> ((All (x,p)) '&' (All (x,q))) is valid proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A for x being bound_QC-variable of A holds (All (x,(p '&' q))) <=> ((All (x,p)) '&' (All (x,q))) is valid let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A holds (All (x,(p '&' q))) <=> ((All (x,p)) '&' (All (x,q))) is valid let x be bound_QC-variable of A; ::_thesis: (All (x,(p '&' q))) <=> ((All (x,p)) '&' (All (x,q))) is valid ( (All (x,(p '&' q))) => ((All (x,p)) '&' (All (x,q))) is valid & ((All (x,p)) '&' (All (x,q))) => (All (x,(p '&' q))) is valid ) by Th36; hence (All (x,(p '&' q))) <=> ((All (x,p)) '&' (All (x,q))) is valid by Lm14; ::_thesis: verum end; theorem :: CQC_THE2:38 for A being QC-alphabet for p, q being Element of CQC-WFF A for x being bound_QC-variable of A holds ( All (x,(p '&' q)) is valid iff (All (x,p)) '&' (All (x,q)) is valid ) proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A for x being bound_QC-variable of A holds ( All (x,(p '&' q)) is valid iff (All (x,p)) '&' (All (x,q)) is valid ) let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A holds ( All (x,(p '&' q)) is valid iff (All (x,p)) '&' (All (x,q)) is valid ) let x be bound_QC-variable of A; ::_thesis: ( All (x,(p '&' q)) is valid iff (All (x,p)) '&' (All (x,q)) is valid ) (All (x,(p '&' q))) <=> ((All (x,p)) '&' (All (x,q))) is valid by Th37; hence ( All (x,(p '&' q)) is valid iff (All (x,p)) '&' (All (x,q)) is valid ) by Lm15; ::_thesis: verum end; theorem Th39: :: CQC_THE2:39 for A being QC-alphabet for p, q being Element of CQC-WFF A for x being bound_QC-variable of A holds ((All (x,p)) 'or' (All (x,q))) => (All (x,(p 'or' q))) is valid proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A for x being bound_QC-variable of A holds ((All (x,p)) 'or' (All (x,q))) => (All (x,(p 'or' q))) is valid let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A holds ((All (x,p)) 'or' (All (x,q))) => (All (x,(p 'or' q))) is valid let x be bound_QC-variable of A; ::_thesis: ((All (x,p)) 'or' (All (x,q))) => (All (x,(p 'or' q))) is valid ( All (x,(q => (p 'or' q))) is valid & (All (x,(q => (p 'or' q)))) => ((All (x,q)) => (All (x,(p 'or' q)))) is valid ) by Lm6, Th23, Th30; then A1: (All (x,q)) => (All (x,(p 'or' q))) is valid by CQC_THE1:65; ( All (x,(p => (p 'or' q))) is valid & (All (x,(p => (p 'or' q)))) => ((All (x,p)) => (All (x,(p 'or' q)))) is valid ) by Lm6, Th23, Th30; then (All (x,p)) => (All (x,(p 'or' q))) is valid by CQC_THE1:65; hence ((All (x,p)) 'or' (All (x,q))) => (All (x,(p 'or' q))) is valid by A1, Lm7; ::_thesis: verum end; theorem Th40: :: CQC_THE2:40 for A being QC-alphabet for p, q being Element of CQC-WFF A for x being bound_QC-variable of A holds ( (Ex (x,(p 'or' q))) => ((Ex (x,p)) 'or' (Ex (x,q))) is valid & ((Ex (x,p)) 'or' (Ex (x,q))) => (Ex (x,(p 'or' q))) is valid ) proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A for x being bound_QC-variable of A holds ( (Ex (x,(p 'or' q))) => ((Ex (x,p)) 'or' (Ex (x,q))) is valid & ((Ex (x,p)) 'or' (Ex (x,q))) => (Ex (x,(p 'or' q))) is valid ) let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A holds ( (Ex (x,(p 'or' q))) => ((Ex (x,p)) 'or' (Ex (x,q))) is valid & ((Ex (x,p)) 'or' (Ex (x,q))) => (Ex (x,(p 'or' q))) is valid ) let x be bound_QC-variable of A; ::_thesis: ( (Ex (x,(p 'or' q))) => ((Ex (x,p)) 'or' (Ex (x,q))) is valid & ((Ex (x,p)) 'or' (Ex (x,q))) => (Ex (x,(p 'or' q))) is valid ) ( not x in still_not-bound_in (Ex (x,p)) & not x in still_not-bound_in (Ex (x,q)) ) by Th6; then A1: not x in still_not-bound_in ((Ex (x,p)) 'or' (Ex (x,q))) by Th9; ( p => (Ex (x,p)) is valid & q => (Ex (x,q)) is valid ) by Th15; then (p 'or' q) => ((Ex (x,p)) 'or' (Ex (x,q))) is valid by Lm4; hence (Ex (x,(p 'or' q))) => ((Ex (x,p)) 'or' (Ex (x,q))) is valid by A1, Th19; ::_thesis: ((Ex (x,p)) 'or' (Ex (x,q))) => (Ex (x,(p 'or' q))) is valid ( All (x,(q => (p 'or' q))) is valid & (All (x,(q => (p 'or' q)))) => ((Ex (x,q)) => (Ex (x,(p 'or' q)))) is valid ) by Lm6, Th23, Th34; then A2: (Ex (x,q)) => (Ex (x,(p 'or' q))) is valid by CQC_THE1:65; ( All (x,(p => (p 'or' q))) is valid & (All (x,(p => (p 'or' q)))) => ((Ex (x,p)) => (Ex (x,(p 'or' q)))) is valid ) by Lm6, Th23, Th34; then (Ex (x,p)) => (Ex (x,(p 'or' q))) is valid by CQC_THE1:65; hence ((Ex (x,p)) 'or' (Ex (x,q))) => (Ex (x,(p 'or' q))) is valid by A2, Lm7; ::_thesis: verum end; theorem Th41: :: CQC_THE2:41 for A being QC-alphabet for p, q being Element of CQC-WFF A for x being bound_QC-variable of A holds (Ex (x,(p 'or' q))) <=> ((Ex (x,p)) 'or' (Ex (x,q))) is valid proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A for x being bound_QC-variable of A holds (Ex (x,(p 'or' q))) <=> ((Ex (x,p)) 'or' (Ex (x,q))) is valid let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A holds (Ex (x,(p 'or' q))) <=> ((Ex (x,p)) 'or' (Ex (x,q))) is valid let x be bound_QC-variable of A; ::_thesis: (Ex (x,(p 'or' q))) <=> ((Ex (x,p)) 'or' (Ex (x,q))) is valid ( (Ex (x,(p 'or' q))) => ((Ex (x,p)) 'or' (Ex (x,q))) is valid & ((Ex (x,p)) 'or' (Ex (x,q))) => (Ex (x,(p 'or' q))) is valid ) by Th40; hence (Ex (x,(p 'or' q))) <=> ((Ex (x,p)) 'or' (Ex (x,q))) is valid by Lm14; ::_thesis: verum end; theorem :: CQC_THE2:42 for A being QC-alphabet for p, q being Element of CQC-WFF A for x being bound_QC-variable of A holds ( Ex (x,(p 'or' q)) is valid iff (Ex (x,p)) 'or' (Ex (x,q)) is valid ) proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A for x being bound_QC-variable of A holds ( Ex (x,(p 'or' q)) is valid iff (Ex (x,p)) 'or' (Ex (x,q)) is valid ) let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A holds ( Ex (x,(p 'or' q)) is valid iff (Ex (x,p)) 'or' (Ex (x,q)) is valid ) let x be bound_QC-variable of A; ::_thesis: ( Ex (x,(p 'or' q)) is valid iff (Ex (x,p)) 'or' (Ex (x,q)) is valid ) (Ex (x,(p 'or' q))) <=> ((Ex (x,p)) 'or' (Ex (x,q))) is valid by Th41; hence ( Ex (x,(p 'or' q)) is valid iff (Ex (x,p)) 'or' (Ex (x,q)) is valid ) by Lm15; ::_thesis: verum end; theorem Th43: :: CQC_THE2:43 for A being QC-alphabet for p, q being Element of CQC-WFF A for x being bound_QC-variable of A holds (Ex (x,(p '&' q))) => ((Ex (x,p)) '&' (Ex (x,q))) is valid proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A for x being bound_QC-variable of A holds (Ex (x,(p '&' q))) => ((Ex (x,p)) '&' (Ex (x,q))) is valid let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A holds (Ex (x,(p '&' q))) => ((Ex (x,p)) '&' (Ex (x,q))) is valid let x be bound_QC-variable of A; ::_thesis: (Ex (x,(p '&' q))) => ((Ex (x,p)) '&' (Ex (x,q))) is valid All (x,((p '&' q) => q)) is valid by Lm1, Th23; then A1: (Ex (x,(p '&' q))) => (Ex (x,q)) is valid by Th35; All (x,((p '&' q) => p)) is valid by Lm1, Th23; then (Ex (x,(p '&' q))) => (Ex (x,p)) is valid by Th35; hence (Ex (x,(p '&' q))) => ((Ex (x,p)) '&' (Ex (x,q))) is valid by A1, Lm3; ::_thesis: verum end; theorem :: CQC_THE2:44 for A being QC-alphabet for p, q being Element of CQC-WFF A for x being bound_QC-variable of A st Ex (x,(p '&' q)) is valid holds (Ex (x,p)) '&' (Ex (x,q)) is valid proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A for x being bound_QC-variable of A st Ex (x,(p '&' q)) is valid holds (Ex (x,p)) '&' (Ex (x,q)) is valid let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A st Ex (x,(p '&' q)) is valid holds (Ex (x,p)) '&' (Ex (x,q)) is valid let x be bound_QC-variable of A; ::_thesis: ( Ex (x,(p '&' q)) is valid implies (Ex (x,p)) '&' (Ex (x,q)) is valid ) assume A1: Ex (x,(p '&' q)) is valid ; ::_thesis: (Ex (x,p)) '&' (Ex (x,q)) is valid (Ex (x,(p '&' q))) => ((Ex (x,p)) '&' (Ex (x,q))) is valid by Th43; hence (Ex (x,p)) '&' (Ex (x,q)) is valid by A1, CQC_THE1:65; ::_thesis: verum end; theorem Th45: :: CQC_THE2:45 for A being QC-alphabet for p being Element of CQC-WFF A for x being bound_QC-variable of A holds ( (All (x,('not' ('not' p)))) => (All (x,p)) is valid & (All (x,p)) => (All (x,('not' ('not' p)))) is valid ) proof let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A for x being bound_QC-variable of A holds ( (All (x,('not' ('not' p)))) => (All (x,p)) is valid & (All (x,p)) => (All (x,('not' ('not' p)))) is valid ) let p be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A holds ( (All (x,('not' ('not' p)))) => (All (x,p)) is valid & (All (x,p)) => (All (x,('not' ('not' p)))) is valid ) let x be bound_QC-variable of A; ::_thesis: ( (All (x,('not' ('not' p)))) => (All (x,p)) is valid & (All (x,p)) => (All (x,('not' ('not' p)))) is valid ) ( All (x,(('not' ('not' p)) => p)) is valid & All (x,(p => ('not' ('not' p)))) is valid ) by Th23; hence ( (All (x,('not' ('not' p)))) => (All (x,p)) is valid & (All (x,p)) => (All (x,('not' ('not' p)))) is valid ) by Th31; ::_thesis: verum end; theorem :: CQC_THE2:46 for A being QC-alphabet for p being Element of CQC-WFF A for x being bound_QC-variable of A holds (All (x,('not' ('not' p)))) <=> (All (x,p)) is valid proof let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A for x being bound_QC-variable of A holds (All (x,('not' ('not' p)))) <=> (All (x,p)) is valid let p be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A holds (All (x,('not' ('not' p)))) <=> (All (x,p)) is valid let x be bound_QC-variable of A; ::_thesis: (All (x,('not' ('not' p)))) <=> (All (x,p)) is valid ( (All (x,('not' ('not' p)))) => (All (x,p)) is valid & (All (x,p)) => (All (x,('not' ('not' p)))) is valid ) by Th45; hence (All (x,('not' ('not' p)))) <=> (All (x,p)) is valid by Lm14; ::_thesis: verum end; theorem Th47: :: CQC_THE2:47 for A being QC-alphabet for p being Element of CQC-WFF A for x being bound_QC-variable of A holds ( (Ex (x,('not' ('not' p)))) => (Ex (x,p)) is valid & (Ex (x,p)) => (Ex (x,('not' ('not' p)))) is valid ) proof let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A for x being bound_QC-variable of A holds ( (Ex (x,('not' ('not' p)))) => (Ex (x,p)) is valid & (Ex (x,p)) => (Ex (x,('not' ('not' p)))) is valid ) let p be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A holds ( (Ex (x,('not' ('not' p)))) => (Ex (x,p)) is valid & (Ex (x,p)) => (Ex (x,('not' ('not' p)))) is valid ) let x be bound_QC-variable of A; ::_thesis: ( (Ex (x,('not' ('not' p)))) => (Ex (x,p)) is valid & (Ex (x,p)) => (Ex (x,('not' ('not' p)))) is valid ) ( All (x,(('not' ('not' p)) => p)) is valid & All (x,(p => ('not' ('not' p)))) is valid ) by Th23; hence ( (Ex (x,('not' ('not' p)))) => (Ex (x,p)) is valid & (Ex (x,p)) => (Ex (x,('not' ('not' p)))) is valid ) by Th35; ::_thesis: verum end; theorem :: CQC_THE2:48 for A being QC-alphabet for p being Element of CQC-WFF A for x being bound_QC-variable of A holds (Ex (x,('not' ('not' p)))) <=> (Ex (x,p)) is valid proof let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A for x being bound_QC-variable of A holds (Ex (x,('not' ('not' p)))) <=> (Ex (x,p)) is valid let p be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A holds (Ex (x,('not' ('not' p)))) <=> (Ex (x,p)) is valid let x be bound_QC-variable of A; ::_thesis: (Ex (x,('not' ('not' p)))) <=> (Ex (x,p)) is valid ( (Ex (x,('not' ('not' p)))) => (Ex (x,p)) is valid & (Ex (x,p)) => (Ex (x,('not' ('not' p)))) is valid ) by Th47; hence (Ex (x,('not' ('not' p)))) <=> (Ex (x,p)) is valid by Lm14; ::_thesis: verum end; theorem Th49: :: CQC_THE2:49 for A being QC-alphabet for p being Element of CQC-WFF A for x being bound_QC-variable of A holds ( ('not' (Ex (x,('not' p)))) => (All (x,p)) is valid & (All (x,p)) => ('not' (Ex (x,('not' p)))) is valid ) proof let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A for x being bound_QC-variable of A holds ( ('not' (Ex (x,('not' p)))) => (All (x,p)) is valid & (All (x,p)) => ('not' (Ex (x,('not' p)))) is valid ) let p be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A holds ( ('not' (Ex (x,('not' p)))) => (All (x,p)) is valid & (All (x,p)) => ('not' (Ex (x,('not' p)))) is valid ) let x be bound_QC-variable of A; ::_thesis: ( ('not' (Ex (x,('not' p)))) => (All (x,p)) is valid & (All (x,p)) => ('not' (Ex (x,('not' p)))) is valid ) A1: (All (x,('not' ('not' p)))) => (All (x,p)) is valid by Th45; A2: 'not' (Ex (x,('not' p))) = 'not' ('not' (All (x,('not' ('not' p))))) by QC_LANG2:def_5; then ('not' (Ex (x,('not' p)))) => (All (x,('not' ('not' p)))) is valid ; hence ('not' (Ex (x,('not' p)))) => (All (x,p)) is valid by A1, LUKASI_1:42; ::_thesis: (All (x,p)) => ('not' (Ex (x,('not' p)))) is valid ( (All (x,p)) => (All (x,('not' ('not' p)))) is valid & (All (x,('not' ('not' p)))) => ('not' ('not' (All (x,('not' ('not' p)))))) is valid ) by Th45; hence (All (x,p)) => ('not' (Ex (x,('not' p)))) is valid by A2, LUKASI_1:42; ::_thesis: verum end; theorem :: CQC_THE2:50 for A being QC-alphabet for p being Element of CQC-WFF A for x being bound_QC-variable of A holds ('not' (Ex (x,('not' p)))) <=> (All (x,p)) is valid proof let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A for x being bound_QC-variable of A holds ('not' (Ex (x,('not' p)))) <=> (All (x,p)) is valid let p be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A holds ('not' (Ex (x,('not' p)))) <=> (All (x,p)) is valid let x be bound_QC-variable of A; ::_thesis: ('not' (Ex (x,('not' p)))) <=> (All (x,p)) is valid ( ('not' (Ex (x,('not' p)))) => (All (x,p)) is valid & (All (x,p)) => ('not' (Ex (x,('not' p)))) is valid ) by Th49; hence ('not' (Ex (x,('not' p)))) <=> (All (x,p)) is valid by Lm14; ::_thesis: verum end; theorem Th51: :: CQC_THE2:51 for A being QC-alphabet for p being Element of CQC-WFF A for x being bound_QC-variable of A holds ( ('not' (All (x,p))) => (Ex (x,('not' p))) is valid & (Ex (x,('not' p))) => ('not' (All (x,p))) is valid ) proof let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A for x being bound_QC-variable of A holds ( ('not' (All (x,p))) => (Ex (x,('not' p))) is valid & (Ex (x,('not' p))) => ('not' (All (x,p))) is valid ) let p be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A holds ( ('not' (All (x,p))) => (Ex (x,('not' p))) is valid & (Ex (x,('not' p))) => ('not' (All (x,p))) is valid ) let x be bound_QC-variable of A; ::_thesis: ( ('not' (All (x,p))) => (Ex (x,('not' p))) is valid & (Ex (x,('not' p))) => ('not' (All (x,p))) is valid ) A1: Ex (x,('not' p)) = 'not' (All (x,('not' ('not' p)))) by QC_LANG2:def_5; (All (x,('not' ('not' p)))) => (All (x,p)) is valid by Th45; hence ('not' (All (x,p))) => (Ex (x,('not' p))) is valid by A1, LUKASI_1:52; ::_thesis: (Ex (x,('not' p))) => ('not' (All (x,p))) is valid (All (x,p)) => (All (x,('not' ('not' p)))) is valid by Th45; hence (Ex (x,('not' p))) => ('not' (All (x,p))) is valid by A1, LUKASI_1:52; ::_thesis: verum end; theorem :: CQC_THE2:52 for A being QC-alphabet for p being Element of CQC-WFF A for x being bound_QC-variable of A holds ('not' (All (x,p))) <=> (Ex (x,('not' p))) is valid proof let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A for x being bound_QC-variable of A holds ('not' (All (x,p))) <=> (Ex (x,('not' p))) is valid let p be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A holds ('not' (All (x,p))) <=> (Ex (x,('not' p))) is valid let x be bound_QC-variable of A; ::_thesis: ('not' (All (x,p))) <=> (Ex (x,('not' p))) is valid ( ('not' (All (x,p))) => (Ex (x,('not' p))) is valid & (Ex (x,('not' p))) => ('not' (All (x,p))) is valid ) by Th51; hence ('not' (All (x,p))) <=> (Ex (x,('not' p))) is valid by Lm14; ::_thesis: verum end; theorem :: CQC_THE2:53 for A being QC-alphabet for p being Element of CQC-WFF A for x being bound_QC-variable of A holds ( ('not' (Ex (x,p))) => (All (x,('not' p))) is valid & (All (x,('not' p))) => ('not' (Ex (x,p))) is valid ) proof let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A for x being bound_QC-variable of A holds ( ('not' (Ex (x,p))) => (All (x,('not' p))) is valid & (All (x,('not' p))) => ('not' (Ex (x,p))) is valid ) let p be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A holds ( ('not' (Ex (x,p))) => (All (x,('not' p))) is valid & (All (x,('not' p))) => ('not' (Ex (x,p))) is valid ) let x be bound_QC-variable of A; ::_thesis: ( ('not' (Ex (x,p))) => (All (x,('not' p))) is valid & (All (x,('not' p))) => ('not' (Ex (x,p))) is valid ) A1: 'not' (Ex (x,p)) = 'not' ('not' (All (x,('not' p)))) by QC_LANG2:def_5; hence ('not' (Ex (x,p))) => (All (x,('not' p))) is valid ; ::_thesis: (All (x,('not' p))) => ('not' (Ex (x,p))) is valid thus (All (x,('not' p))) => ('not' (Ex (x,p))) is valid by A1; ::_thesis: verum end; theorem Th54: :: CQC_THE2:54 for A being QC-alphabet for p being Element of CQC-WFF A for x being bound_QC-variable of A holds (All (x,('not' p))) <=> ('not' (Ex (x,p))) is valid proof let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A for x being bound_QC-variable of A holds (All (x,('not' p))) <=> ('not' (Ex (x,p))) is valid let p be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A holds (All (x,('not' p))) <=> ('not' (Ex (x,p))) is valid let x be bound_QC-variable of A; ::_thesis: (All (x,('not' p))) <=> ('not' (Ex (x,p))) is valid ('not' ('not' (All (x,('not' p))))) => (All (x,('not' p))) is valid ; then A1: ('not' (Ex (x,p))) => (All (x,('not' p))) is valid by QC_LANG2:def_5; (All (x,('not' p))) => ('not' ('not' (All (x,('not' p))))) is valid ; then (All (x,('not' p))) => ('not' (Ex (x,p))) is valid by QC_LANG2:def_5; hence (All (x,('not' p))) <=> ('not' (Ex (x,p))) is valid by A1, Lm14; ::_thesis: verum end; theorem :: CQC_THE2:55 for A being QC-alphabet for p being Element of CQC-WFF A for x, y being bound_QC-variable of A holds ( (All (x,(All (y,p)))) => (All (y,(All (x,p)))) is valid & (All (x,y,p)) => (All (y,x,p)) is valid ) proof let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A for x, y being bound_QC-variable of A holds ( (All (x,(All (y,p)))) => (All (y,(All (x,p)))) is valid & (All (x,y,p)) => (All (y,x,p)) is valid ) let p be Element of CQC-WFF A; ::_thesis: for x, y being bound_QC-variable of A holds ( (All (x,(All (y,p)))) => (All (y,(All (x,p)))) is valid & (All (x,y,p)) => (All (y,x,p)) is valid ) let x, y be bound_QC-variable of A; ::_thesis: ( (All (x,(All (y,p)))) => (All (y,(All (x,p)))) is valid & (All (x,y,p)) => (All (y,x,p)) is valid ) not y in still_not-bound_in (All (y,p)) by Th5; then A1: not y in still_not-bound_in (All (x,(All (y,p)))) by Th5; ( All (x,((All (y,p)) => p)) is valid & (All (x,((All (y,p)) => p))) => ((All (x,(All (y,p)))) => (All (x,p))) is valid ) by Th23, Th30, CQC_THE1:66; then (All (x,(All (y,p)))) => (All (x,p)) is valid by CQC_THE1:65; hence (All (x,(All (y,p)))) => (All (y,(All (x,p)))) is valid by A1, CQC_THE1:67; ::_thesis: (All (x,y,p)) => (All (y,x,p)) is valid then (All (x,y,p)) => (All (y,(All (x,p)))) is valid by QC_LANG2:14; hence (All (x,y,p)) => (All (y,x,p)) is valid by QC_LANG2:14; ::_thesis: verum end; theorem :: CQC_THE2:56 for A being QC-alphabet for p, q being Element of CQC-WFF A for h being QC-formula of A for x, y being bound_QC-variable of A st p = h . x & q = h . y & not y in still_not-bound_in h holds (All (x,(All (y,q)))) => (All (x,p)) is valid proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A for h being QC-formula of A for x, y being bound_QC-variable of A st p = h . x & q = h . y & not y in still_not-bound_in h holds (All (x,(All (y,q)))) => (All (x,p)) is valid let p, q be Element of CQC-WFF A; ::_thesis: for h being QC-formula of A for x, y being bound_QC-variable of A st p = h . x & q = h . y & not y in still_not-bound_in h holds (All (x,(All (y,q)))) => (All (x,p)) is valid let h be QC-formula of A; ::_thesis: for x, y being bound_QC-variable of A st p = h . x & q = h . y & not y in still_not-bound_in h holds (All (x,(All (y,q)))) => (All (x,p)) is valid let x, y be bound_QC-variable of A; ::_thesis: ( p = h . x & q = h . y & not y in still_not-bound_in h implies (All (x,(All (y,q)))) => (All (x,p)) is valid ) assume ( p = h . x & q = h . y & not y in still_not-bound_in h ) ; ::_thesis: (All (x,(All (y,q)))) => (All (x,p)) is valid then All (x,((All (y,q)) => p)) is valid by Th23, Th25; hence (All (x,(All (y,q)))) => (All (x,p)) is valid by Th31; ::_thesis: verum end; theorem :: CQC_THE2:57 for A being QC-alphabet for p being Element of CQC-WFF A for x, y being bound_QC-variable of A holds ( (Ex (x,(Ex (y,p)))) => (Ex (y,(Ex (x,p)))) is valid & (Ex (x,y,p)) => (Ex (y,x,p)) is valid ) proof let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A for x, y being bound_QC-variable of A holds ( (Ex (x,(Ex (y,p)))) => (Ex (y,(Ex (x,p)))) is valid & (Ex (x,y,p)) => (Ex (y,x,p)) is valid ) let p be Element of CQC-WFF A; ::_thesis: for x, y being bound_QC-variable of A holds ( (Ex (x,(Ex (y,p)))) => (Ex (y,(Ex (x,p)))) is valid & (Ex (x,y,p)) => (Ex (y,x,p)) is valid ) let x, y be bound_QC-variable of A; ::_thesis: ( (Ex (x,(Ex (y,p)))) => (Ex (y,(Ex (x,p)))) is valid & (Ex (x,y,p)) => (Ex (y,x,p)) is valid ) not x in still_not-bound_in (Ex (x,p)) by Th6; then A1: not x in still_not-bound_in (Ex (y,(Ex (x,p)))) by Th6; ( All (y,(p => (Ex (x,p)))) is valid & (All (y,(p => (Ex (x,p))))) => ((Ex (y,p)) => (Ex (y,(Ex (x,p))))) is valid ) by Th15, Th23, Th34; then (Ex (y,p)) => (Ex (y,(Ex (x,p)))) is valid by CQC_THE1:65; hence (Ex (x,(Ex (y,p)))) => (Ex (y,(Ex (x,p)))) is valid by A1, Th19; ::_thesis: (Ex (x,y,p)) => (Ex (y,x,p)) is valid then (Ex (x,y,p)) => (Ex (y,(Ex (x,p)))) is valid by QC_LANG2:14; hence (Ex (x,y,p)) => (Ex (y,x,p)) is valid by QC_LANG2:14; ::_thesis: verum end; theorem :: CQC_THE2:58 for A being QC-alphabet for p, q being Element of CQC-WFF A for h being QC-formula of A for x, y being bound_QC-variable of A st p = h . x & q = h . y & not y in still_not-bound_in h holds (Ex (x,p)) => (Ex (x,y,q)) is valid proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A for h being QC-formula of A for x, y being bound_QC-variable of A st p = h . x & q = h . y & not y in still_not-bound_in h holds (Ex (x,p)) => (Ex (x,y,q)) is valid let p, q be Element of CQC-WFF A; ::_thesis: for h being QC-formula of A for x, y being bound_QC-variable of A st p = h . x & q = h . y & not y in still_not-bound_in h holds (Ex (x,p)) => (Ex (x,y,q)) is valid let h be QC-formula of A; ::_thesis: for x, y being bound_QC-variable of A st p = h . x & q = h . y & not y in still_not-bound_in h holds (Ex (x,p)) => (Ex (x,y,q)) is valid let x, y be bound_QC-variable of A; ::_thesis: ( p = h . x & q = h . y & not y in still_not-bound_in h implies (Ex (x,p)) => (Ex (x,y,q)) is valid ) assume ( p = h . x & q = h . y & not y in still_not-bound_in h ) ; ::_thesis: (Ex (x,p)) => (Ex (x,y,q)) is valid then All (x,(p => (Ex (y,q)))) is valid by Th22, Th23; then (Ex (x,p)) => (Ex (x,(Ex (y,q)))) is valid by Th35; hence (Ex (x,p)) => (Ex (x,y,q)) is valid by QC_LANG2:14; ::_thesis: verum end; theorem :: CQC_THE2:59 for A being QC-alphabet for p being Element of CQC-WFF A for x, y being bound_QC-variable of A holds (Ex (x,(All (y,p)))) => (All (y,(Ex (x,p)))) is valid proof let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A for x, y being bound_QC-variable of A holds (Ex (x,(All (y,p)))) => (All (y,(Ex (x,p)))) is valid let p be Element of CQC-WFF A; ::_thesis: for x, y being bound_QC-variable of A holds (Ex (x,(All (y,p)))) => (All (y,(Ex (x,p)))) is valid let x, y be bound_QC-variable of A; ::_thesis: (Ex (x,(All (y,p)))) => (All (y,(Ex (x,p)))) is valid not x in still_not-bound_in (Ex (x,p)) by Th6; then A1: not x in still_not-bound_in (All (y,(Ex (x,p)))) by Th5; ( All (y,(p => (Ex (x,p)))) is valid & (All (y,(p => (Ex (x,p))))) => ((All (y,p)) => (All (y,(Ex (x,p))))) is valid ) by Th15, Th23, Th30; then (All (y,p)) => (All (y,(Ex (x,p)))) is valid by CQC_THE1:65; hence (Ex (x,(All (y,p)))) => (All (y,(Ex (x,p)))) is valid by A1, Th19; ::_thesis: verum end; theorem :: CQC_THE2:60 for A being QC-alphabet for p being Element of CQC-WFF A for x being bound_QC-variable of A holds Ex (x,(p <=> p)) is valid by Lm13, Th16; theorem Th61: :: CQC_THE2:61 for A being QC-alphabet for p, q being Element of CQC-WFF A for x being bound_QC-variable of A holds ( (Ex (x,(p => q))) => ((All (x,p)) => (Ex (x,q))) is valid & ((All (x,p)) => (Ex (x,q))) => (Ex (x,(p => q))) is valid ) proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A for x being bound_QC-variable of A holds ( (Ex (x,(p => q))) => ((All (x,p)) => (Ex (x,q))) is valid & ((All (x,p)) => (Ex (x,q))) => (Ex (x,(p => q))) is valid ) let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A holds ( (Ex (x,(p => q))) => ((All (x,p)) => (Ex (x,q))) is valid & ((All (x,p)) => (Ex (x,q))) => (Ex (x,(p => q))) is valid ) let x be bound_QC-variable of A; ::_thesis: ( (Ex (x,(p => q))) => ((All (x,p)) => (Ex (x,q))) is valid & ((All (x,p)) => (Ex (x,q))) => (Ex (x,(p => q))) is valid ) (All (x,p)) => p is valid by CQC_THE1:66; then A1: (p => q) => ((All (x,p)) => q) is valid by LUKASI_1:41; ( not x in still_not-bound_in (All (x,p)) & not x in still_not-bound_in (Ex (x,q)) ) by Th5, Th6; then A2: not x in still_not-bound_in ((All (x,p)) => (Ex (x,q))) by Th7; q => (Ex (x,q)) is valid by Th15; then (p => q) => ((All (x,p)) => (Ex (x,q))) is valid by A1, Lm16; hence (Ex (x,(p => q))) => ((All (x,p)) => (Ex (x,q))) is valid by A2, Th19; ::_thesis: ((All (x,p)) => (Ex (x,q))) => (Ex (x,(p => q))) is valid (All (x,(p '&' ('not' q)))) => ((All (x,p)) '&' (All (x,('not' q)))) is valid by Th36; then A3: ('not' ((All (x,p)) '&' (All (x,('not' q))))) => ('not' (All (x,(p '&' ('not' q))))) is valid by LUKASI_1:52; ('not' (All (x,(p '&' ('not' q))))) => (Ex (x,('not' (p '&' ('not' q))))) is valid by Th51; then ('not' ((All (x,p)) '&' (All (x,('not' q))))) => (Ex (x,('not' (p '&' ('not' q))))) is valid by A3, LUKASI_1:42; then A4: ('not' ((All (x,p)) '&' (All (x,('not' q))))) => (Ex (x,(p => q))) is valid by QC_LANG2:def_2; (All (x,('not' q))) => ('not' ('not' (All (x,('not' q))))) is valid ; then A5: ((All (x,p)) '&' (All (x,('not' q)))) => ((All (x,p)) '&' ('not' ('not' (All (x,('not' q)))))) is valid by Lm9; (All (x,p)) => (Ex (x,q)) = (All (x,p)) => ('not' (All (x,('not' q)))) by QC_LANG2:def_5 .= 'not' ((All (x,p)) '&' ('not' ('not' (All (x,('not' q)))))) by QC_LANG2:def_2 ; then ((All (x,p)) => (Ex (x,q))) => ('not' ((All (x,p)) '&' (All (x,('not' q))))) is valid by A5, LUKASI_1:52; hence ((All (x,p)) => (Ex (x,q))) => (Ex (x,(p => q))) is valid by A4, LUKASI_1:42; ::_thesis: verum end; theorem Th62: :: CQC_THE2:62 for A being QC-alphabet for p, q being Element of CQC-WFF A for x being bound_QC-variable of A holds (Ex (x,(p => q))) <=> ((All (x,p)) => (Ex (x,q))) is valid proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A for x being bound_QC-variable of A holds (Ex (x,(p => q))) <=> ((All (x,p)) => (Ex (x,q))) is valid let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A holds (Ex (x,(p => q))) <=> ((All (x,p)) => (Ex (x,q))) is valid let x be bound_QC-variable of A; ::_thesis: (Ex (x,(p => q))) <=> ((All (x,p)) => (Ex (x,q))) is valid ( (Ex (x,(p => q))) => ((All (x,p)) => (Ex (x,q))) is valid & ((All (x,p)) => (Ex (x,q))) => (Ex (x,(p => q))) is valid ) by Th61; hence (Ex (x,(p => q))) <=> ((All (x,p)) => (Ex (x,q))) is valid by Lm14; ::_thesis: verum end; theorem :: CQC_THE2:63 for A being QC-alphabet for p, q being Element of CQC-WFF A for x being bound_QC-variable of A holds ( Ex (x,(p => q)) is valid iff (All (x,p)) => (Ex (x,q)) is valid ) proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A for x being bound_QC-variable of A holds ( Ex (x,(p => q)) is valid iff (All (x,p)) => (Ex (x,q)) is valid ) let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A holds ( Ex (x,(p => q)) is valid iff (All (x,p)) => (Ex (x,q)) is valid ) let x be bound_QC-variable of A; ::_thesis: ( Ex (x,(p => q)) is valid iff (All (x,p)) => (Ex (x,q)) is valid ) (Ex (x,(p => q))) <=> ((All (x,p)) => (Ex (x,q))) is valid by Th62; hence ( Ex (x,(p => q)) is valid iff (All (x,p)) => (Ex (x,q)) is valid ) by Lm15; ::_thesis: verum end; theorem Th64: :: CQC_THE2:64 for A being QC-alphabet for p, q being Element of CQC-WFF A for x being bound_QC-variable of A holds (All (x,(p '&' q))) => (p '&' (All (x,q))) is valid proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A for x being bound_QC-variable of A holds (All (x,(p '&' q))) => (p '&' (All (x,q))) is valid let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A holds (All (x,(p '&' q))) => (p '&' (All (x,q))) is valid let x be bound_QC-variable of A; ::_thesis: (All (x,(p '&' q))) => (p '&' (All (x,q))) is valid A1: (All (x,(p '&' q))) => (p '&' q) is valid by CQC_THE1:66; A2: not x in still_not-bound_in (All (x,(p '&' q))) by Th5; (p '&' q) => q is valid by Lm1; then (All (x,(p '&' q))) => q is valid by A1, LUKASI_1:42; then A3: (All (x,(p '&' q))) => (All (x,q)) is valid by A2, CQC_THE1:67; (p '&' q) => p is valid by Lm1; then (All (x,(p '&' q))) => p is valid by A1, LUKASI_1:42; hence (All (x,(p '&' q))) => (p '&' (All (x,q))) is valid by A3, Lm3; ::_thesis: verum end; theorem Th65: :: CQC_THE2:65 for A being QC-alphabet for p, q being Element of CQC-WFF A for x being bound_QC-variable of A holds (All (x,(p '&' q))) => ((All (x,p)) '&' q) is valid proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A for x being bound_QC-variable of A holds (All (x,(p '&' q))) => ((All (x,p)) '&' q) is valid let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A holds (All (x,(p '&' q))) => ((All (x,p)) '&' q) is valid let x be bound_QC-variable of A; ::_thesis: (All (x,(p '&' q))) => ((All (x,p)) '&' q) is valid A1: (q '&' (All (x,p))) => ((All (x,p)) '&' q) is valid by CQC_THE1:64; ( All (x,((p '&' q) => (q '&' p))) is valid & (All (x,((p '&' q) => (q '&' p)))) => ((All (x,(p '&' q))) => (All (x,(q '&' p)))) is valid ) by Th23, Th30, CQC_THE1:64; then A2: (All (x,(p '&' q))) => (All (x,(q '&' p))) is valid by CQC_THE1:65; (All (x,(q '&' p))) => (q '&' (All (x,p))) is valid by Th64; then (All (x,(p '&' q))) => (q '&' (All (x,p))) is valid by A2, LUKASI_1:42; hence (All (x,(p '&' q))) => ((All (x,p)) '&' q) is valid by A1, LUKASI_1:42; ::_thesis: verum end; theorem Th66: :: CQC_THE2:66 for A being QC-alphabet for p, q being Element of CQC-WFF A for x being bound_QC-variable of A st not x in still_not-bound_in p holds (p '&' (All (x,q))) => (All (x,(p '&' q))) is valid proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A for x being bound_QC-variable of A st not x in still_not-bound_in p holds (p '&' (All (x,q))) => (All (x,(p '&' q))) is valid let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A st not x in still_not-bound_in p holds (p '&' (All (x,q))) => (All (x,(p '&' q))) is valid let x be bound_QC-variable of A; ::_thesis: ( not x in still_not-bound_in p implies (p '&' (All (x,q))) => (All (x,(p '&' q))) is valid ) assume A1: not x in still_not-bound_in p ; ::_thesis: (p '&' (All (x,q))) => (All (x,(p '&' q))) is valid (All (x,q)) => q is valid by CQC_THE1:66; then A2: (p '&' (All (x,q))) => (p '&' q) is valid by Lm9; not x in still_not-bound_in (All (x,q)) by Th5; then not x in still_not-bound_in (p '&' (All (x,q))) by A1, Th8; hence (p '&' (All (x,q))) => (All (x,(p '&' q))) is valid by A2, CQC_THE1:67; ::_thesis: verum end; theorem :: CQC_THE2:67 for A being QC-alphabet for p, q being Element of CQC-WFF A for x being bound_QC-variable of A st not x in still_not-bound_in p & p '&' (All (x,q)) is valid holds All (x,(p '&' q)) is valid proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A for x being bound_QC-variable of A st not x in still_not-bound_in p & p '&' (All (x,q)) is valid holds All (x,(p '&' q)) is valid let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A st not x in still_not-bound_in p & p '&' (All (x,q)) is valid holds All (x,(p '&' q)) is valid let x be bound_QC-variable of A; ::_thesis: ( not x in still_not-bound_in p & p '&' (All (x,q)) is valid implies All (x,(p '&' q)) is valid ) assume that A1: not x in still_not-bound_in p and A2: p '&' (All (x,q)) is valid ; ::_thesis: All (x,(p '&' q)) is valid (p '&' (All (x,q))) => (All (x,(p '&' q))) is valid by A1, Th66; hence All (x,(p '&' q)) is valid by A2, CQC_THE1:65; ::_thesis: verum end; theorem Th68: :: CQC_THE2:68 for A being QC-alphabet for p, q being Element of CQC-WFF A for x being bound_QC-variable of A st not x in still_not-bound_in p holds ( (p 'or' (All (x,q))) => (All (x,(p 'or' q))) is valid & (All (x,(p 'or' q))) => (p 'or' (All (x,q))) is valid ) proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A for x being bound_QC-variable of A st not x in still_not-bound_in p holds ( (p 'or' (All (x,q))) => (All (x,(p 'or' q))) is valid & (All (x,(p 'or' q))) => (p 'or' (All (x,q))) is valid ) let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A st not x in still_not-bound_in p holds ( (p 'or' (All (x,q))) => (All (x,(p 'or' q))) is valid & (All (x,(p 'or' q))) => (p 'or' (All (x,q))) is valid ) let x be bound_QC-variable of A; ::_thesis: ( not x in still_not-bound_in p implies ( (p 'or' (All (x,q))) => (All (x,(p 'or' q))) is valid & (All (x,(p 'or' q))) => (p 'or' (All (x,q))) is valid ) ) A1: not x in still_not-bound_in (All (x,(p 'or' q))) by Th5; ( (All (x,(p 'or' q))) => (p 'or' q) is valid & (p 'or' q) => (('not' p) => q) is valid ) by Lm11, CQC_THE1:66; then (All (x,(p 'or' q))) => (('not' p) => q) is valid by LUKASI_1:42; then A2: ((All (x,(p 'or' q))) '&' ('not' p)) => q is valid by Th1; assume A3: not x in still_not-bound_in p ; ::_thesis: ( (p 'or' (All (x,q))) => (All (x,(p 'or' q))) is valid & (All (x,(p 'or' q))) => (p 'or' (All (x,q))) is valid ) then not x in still_not-bound_in ('not' p) by QC_LANG3:7; then not x in still_not-bound_in ((All (x,(p 'or' q))) '&' ('not' p)) by A1, Th8; then ((All (x,(p 'or' q))) '&' ('not' p)) => (All (x,q)) is valid by A2, CQC_THE1:67; then A4: (All (x,(p 'or' q))) => (('not' p) => (All (x,q))) is valid by Th3; p => p is valid ; then p => (All (x,p)) is valid by A3, CQC_THE1:67; then A5: (p 'or' (All (x,q))) => ((All (x,p)) 'or' (All (x,q))) is valid by Lm10; ((All (x,p)) 'or' (All (x,q))) => (All (x,(p 'or' q))) is valid by Th39; hence (p 'or' (All (x,q))) => (All (x,(p 'or' q))) is valid by A5, LUKASI_1:42; ::_thesis: (All (x,(p 'or' q))) => (p 'or' (All (x,q))) is valid (('not' p) => (All (x,q))) => (p 'or' (All (x,q))) is valid by Lm12; hence (All (x,(p 'or' q))) => (p 'or' (All (x,q))) is valid by A4, LUKASI_1:42; ::_thesis: verum end; theorem Th69: :: CQC_THE2:69 for A being QC-alphabet for p, q being Element of CQC-WFF A for x being bound_QC-variable of A st not x in still_not-bound_in p holds (p 'or' (All (x,q))) <=> (All (x,(p 'or' q))) is valid proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A for x being bound_QC-variable of A st not x in still_not-bound_in p holds (p 'or' (All (x,q))) <=> (All (x,(p 'or' q))) is valid let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A st not x in still_not-bound_in p holds (p 'or' (All (x,q))) <=> (All (x,(p 'or' q))) is valid let x be bound_QC-variable of A; ::_thesis: ( not x in still_not-bound_in p implies (p 'or' (All (x,q))) <=> (All (x,(p 'or' q))) is valid ) assume not x in still_not-bound_in p ; ::_thesis: (p 'or' (All (x,q))) <=> (All (x,(p 'or' q))) is valid then ( (p 'or' (All (x,q))) => (All (x,(p 'or' q))) is valid & (All (x,(p 'or' q))) => (p 'or' (All (x,q))) is valid ) by Th68; hence (p 'or' (All (x,q))) <=> (All (x,(p 'or' q))) is valid by Lm14; ::_thesis: verum end; theorem :: CQC_THE2:70 for A being QC-alphabet for p, q being Element of CQC-WFF A for x being bound_QC-variable of A st not x in still_not-bound_in p holds ( p 'or' (All (x,q)) is valid iff All (x,(p 'or' q)) is valid ) proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A for x being bound_QC-variable of A st not x in still_not-bound_in p holds ( p 'or' (All (x,q)) is valid iff All (x,(p 'or' q)) is valid ) let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A st not x in still_not-bound_in p holds ( p 'or' (All (x,q)) is valid iff All (x,(p 'or' q)) is valid ) let x be bound_QC-variable of A; ::_thesis: ( not x in still_not-bound_in p implies ( p 'or' (All (x,q)) is valid iff All (x,(p 'or' q)) is valid ) ) assume not x in still_not-bound_in p ; ::_thesis: ( p 'or' (All (x,q)) is valid iff All (x,(p 'or' q)) is valid ) then (p 'or' (All (x,q))) <=> (All (x,(p 'or' q))) is valid by Th69; hence ( p 'or' (All (x,q)) is valid iff All (x,(p 'or' q)) is valid ) by Lm15; ::_thesis: verum end; theorem Th71: :: CQC_THE2:71 for A being QC-alphabet for p, q being Element of CQC-WFF A for x being bound_QC-variable of A st not x in still_not-bound_in p holds ( (p '&' (Ex (x,q))) => (Ex (x,(p '&' q))) is valid & (Ex (x,(p '&' q))) => (p '&' (Ex (x,q))) is valid ) proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A for x being bound_QC-variable of A st not x in still_not-bound_in p holds ( (p '&' (Ex (x,q))) => (Ex (x,(p '&' q))) is valid & (Ex (x,(p '&' q))) => (p '&' (Ex (x,q))) is valid ) let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A st not x in still_not-bound_in p holds ( (p '&' (Ex (x,q))) => (Ex (x,(p '&' q))) is valid & (Ex (x,(p '&' q))) => (p '&' (Ex (x,q))) is valid ) let x be bound_QC-variable of A; ::_thesis: ( not x in still_not-bound_in p implies ( (p '&' (Ex (x,q))) => (Ex (x,(p '&' q))) is valid & (Ex (x,(p '&' q))) => (p '&' (Ex (x,q))) is valid ) ) assume A1: not x in still_not-bound_in p ; ::_thesis: ( (p '&' (Ex (x,q))) => (Ex (x,(p '&' q))) is valid & (Ex (x,(p '&' q))) => (p '&' (Ex (x,q))) is valid ) (p '&' q) => (Ex (x,(p '&' q))) is valid by Th15; then A2: q => (p => (Ex (x,(p '&' q)))) is valid by Th4; not x in still_not-bound_in (Ex (x,(p '&' q))) by Th6; then not x in still_not-bound_in (p => (Ex (x,(p '&' q)))) by A1, Th7; then (Ex (x,q)) => (p => (Ex (x,(p '&' q)))) is valid by A2, Th19; hence (p '&' (Ex (x,q))) => (Ex (x,(p '&' q))) is valid by Th2; ::_thesis: (Ex (x,(p '&' q))) => (p '&' (Ex (x,q))) is valid q => (Ex (x,q)) is valid by Th15; then A3: (p '&' q) => (p '&' (Ex (x,q))) is valid by Lm9; not x in still_not-bound_in (Ex (x,q)) by Th6; then not x in still_not-bound_in (p '&' (Ex (x,q))) by A1, Th8; hence (Ex (x,(p '&' q))) => (p '&' (Ex (x,q))) is valid by A3, Th19; ::_thesis: verum end; theorem Th72: :: CQC_THE2:72 for A being QC-alphabet for p, q being Element of CQC-WFF A for x being bound_QC-variable of A st not x in still_not-bound_in p holds (p '&' (Ex (x,q))) <=> (Ex (x,(p '&' q))) is valid proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A for x being bound_QC-variable of A st not x in still_not-bound_in p holds (p '&' (Ex (x,q))) <=> (Ex (x,(p '&' q))) is valid let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A st not x in still_not-bound_in p holds (p '&' (Ex (x,q))) <=> (Ex (x,(p '&' q))) is valid let x be bound_QC-variable of A; ::_thesis: ( not x in still_not-bound_in p implies (p '&' (Ex (x,q))) <=> (Ex (x,(p '&' q))) is valid ) assume not x in still_not-bound_in p ; ::_thesis: (p '&' (Ex (x,q))) <=> (Ex (x,(p '&' q))) is valid then ( (p '&' (Ex (x,q))) => (Ex (x,(p '&' q))) is valid & (Ex (x,(p '&' q))) => (p '&' (Ex (x,q))) is valid ) by Th71; hence (p '&' (Ex (x,q))) <=> (Ex (x,(p '&' q))) is valid by Lm14; ::_thesis: verum end; theorem :: CQC_THE2:73 for A being QC-alphabet for p, q being Element of CQC-WFF A for x being bound_QC-variable of A st not x in still_not-bound_in p holds ( p '&' (Ex (x,q)) is valid iff Ex (x,(p '&' q)) is valid ) proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A for x being bound_QC-variable of A st not x in still_not-bound_in p holds ( p '&' (Ex (x,q)) is valid iff Ex (x,(p '&' q)) is valid ) let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A st not x in still_not-bound_in p holds ( p '&' (Ex (x,q)) is valid iff Ex (x,(p '&' q)) is valid ) let x be bound_QC-variable of A; ::_thesis: ( not x in still_not-bound_in p implies ( p '&' (Ex (x,q)) is valid iff Ex (x,(p '&' q)) is valid ) ) assume not x in still_not-bound_in p ; ::_thesis: ( p '&' (Ex (x,q)) is valid iff Ex (x,(p '&' q)) is valid ) then (p '&' (Ex (x,q))) <=> (Ex (x,(p '&' q))) is valid by Th72; hence ( p '&' (Ex (x,q)) is valid iff Ex (x,(p '&' q)) is valid ) by Lm15; ::_thesis: verum end; Lm17: for A being QC-alphabet for p, q being Element of CQC-WFF A for x being bound_QC-variable of A st not x in still_not-bound_in p holds (All (x,(p => q))) => (p => (All (x,q))) is valid proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A for x being bound_QC-variable of A st not x in still_not-bound_in p holds (All (x,(p => q))) => (p => (All (x,q))) is valid let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A st not x in still_not-bound_in p holds (All (x,(p => q))) => (p => (All (x,q))) is valid let x be bound_QC-variable of A; ::_thesis: ( not x in still_not-bound_in p implies (All (x,(p => q))) => (p => (All (x,q))) is valid ) assume not x in still_not-bound_in p ; ::_thesis: (All (x,(p => q))) => (p => (All (x,q))) is valid then A1: p => (All (x,p)) is valid by Th24; (All (x,(p => q))) => ((All (x,p)) => (All (x,q))) is valid by Th30; then (All (x,p)) => ((All (x,(p => q))) => (All (x,q))) is valid by LUKASI_1:44; then p => ((All (x,(p => q))) => (All (x,q))) is valid by A1, LUKASI_1:42; hence (All (x,(p => q))) => (p => (All (x,q))) is valid by LUKASI_1:44; ::_thesis: verum end; theorem Th74: :: CQC_THE2:74 for A being QC-alphabet for p, q being Element of CQC-WFF A for x being bound_QC-variable of A st not x in still_not-bound_in p holds ( (All (x,(p => q))) => (p => (All (x,q))) is valid & (p => (All (x,q))) => (All (x,(p => q))) is valid ) proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A for x being bound_QC-variable of A st not x in still_not-bound_in p holds ( (All (x,(p => q))) => (p => (All (x,q))) is valid & (p => (All (x,q))) => (All (x,(p => q))) is valid ) let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A st not x in still_not-bound_in p holds ( (All (x,(p => q))) => (p => (All (x,q))) is valid & (p => (All (x,q))) => (All (x,(p => q))) is valid ) let x be bound_QC-variable of A; ::_thesis: ( not x in still_not-bound_in p implies ( (All (x,(p => q))) => (p => (All (x,q))) is valid & (p => (All (x,q))) => (All (x,(p => q))) is valid ) ) assume A1: not x in still_not-bound_in p ; ::_thesis: ( (All (x,(p => q))) => (p => (All (x,q))) is valid & (p => (All (x,q))) => (All (x,(p => q))) is valid ) hence (All (x,(p => q))) => (p => (All (x,q))) is valid by Lm17; ::_thesis: (p => (All (x,q))) => (All (x,(p => q))) is valid not x in still_not-bound_in (All (x,q)) by Th5; then not x in still_not-bound_in (p => (All (x,q))) by A1, Th7; then A2: (All (x,((p => (All (x,q))) => (p => q)))) => ((p => (All (x,q))) => (All (x,(p => q)))) is valid by Lm17; ( All (x,(((All (x,q)) => q) => ((p => (All (x,q))) => (p => q)))) is valid & (All (x,(((All (x,q)) => q) => ((p => (All (x,q))) => (p => q))))) => ((All (x,((All (x,q)) => q))) => (All (x,((p => (All (x,q))) => (p => q))))) is valid ) by Th23, Th30; then A3: (All (x,((All (x,q)) => q))) => (All (x,((p => (All (x,q))) => (p => q)))) is valid by CQC_THE1:65; All (x,((All (x,q)) => q)) is valid by Th23, CQC_THE1:66; then All (x,((p => (All (x,q))) => (p => q))) is valid by A3, CQC_THE1:65; hence (p => (All (x,q))) => (All (x,(p => q))) is valid by A2, CQC_THE1:65; ::_thesis: verum end; theorem Th75: :: CQC_THE2:75 for A being QC-alphabet for p, q being Element of CQC-WFF A for x being bound_QC-variable of A st not x in still_not-bound_in p holds (p => (All (x,q))) <=> (All (x,(p => q))) is valid proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A for x being bound_QC-variable of A st not x in still_not-bound_in p holds (p => (All (x,q))) <=> (All (x,(p => q))) is valid let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A st not x in still_not-bound_in p holds (p => (All (x,q))) <=> (All (x,(p => q))) is valid let x be bound_QC-variable of A; ::_thesis: ( not x in still_not-bound_in p implies (p => (All (x,q))) <=> (All (x,(p => q))) is valid ) assume not x in still_not-bound_in p ; ::_thesis: (p => (All (x,q))) <=> (All (x,(p => q))) is valid then ( (p => (All (x,q))) => (All (x,(p => q))) is valid & (All (x,(p => q))) => (p => (All (x,q))) is valid ) by Th74; hence (p => (All (x,q))) <=> (All (x,(p => q))) is valid by Lm14; ::_thesis: verum end; theorem :: CQC_THE2:76 for A being QC-alphabet for p, q being Element of CQC-WFF A for x being bound_QC-variable of A st not x in still_not-bound_in p holds ( All (x,(p => q)) is valid iff p => (All (x,q)) is valid ) proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A for x being bound_QC-variable of A st not x in still_not-bound_in p holds ( All (x,(p => q)) is valid iff p => (All (x,q)) is valid ) let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A st not x in still_not-bound_in p holds ( All (x,(p => q)) is valid iff p => (All (x,q)) is valid ) let x be bound_QC-variable of A; ::_thesis: ( not x in still_not-bound_in p implies ( All (x,(p => q)) is valid iff p => (All (x,q)) is valid ) ) assume not x in still_not-bound_in p ; ::_thesis: ( All (x,(p => q)) is valid iff p => (All (x,q)) is valid ) then (p => (All (x,q))) <=> (All (x,(p => q))) is valid by Th75; hence ( All (x,(p => q)) is valid iff p => (All (x,q)) is valid ) by Lm15; ::_thesis: verum end; theorem Th77: :: CQC_THE2:77 for A being QC-alphabet for q, p being Element of CQC-WFF A for x being bound_QC-variable of A st not x in still_not-bound_in q holds (Ex (x,(p => q))) => ((All (x,p)) => q) is valid proof let A be QC-alphabet ; ::_thesis: for q, p being Element of CQC-WFF A for x being bound_QC-variable of A st not x in still_not-bound_in q holds (Ex (x,(p => q))) => ((All (x,p)) => q) is valid let q, p be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A st not x in still_not-bound_in q holds (Ex (x,(p => q))) => ((All (x,p)) => q) is valid let x be bound_QC-variable of A; ::_thesis: ( not x in still_not-bound_in q implies (Ex (x,(p => q))) => ((All (x,p)) => q) is valid ) assume A1: not x in still_not-bound_in q ; ::_thesis: (Ex (x,(p => q))) => ((All (x,p)) => q) is valid not x in still_not-bound_in (All (x,p)) by Th5; then not x in still_not-bound_in ((All (x,p)) => q) by A1, Th7; then A2: (Ex (x,((All (x,p)) => q))) => ((All (x,p)) => q) is valid by Th20; (All (x,p)) => p is valid by CQC_THE1:66; then A3: All (x,((p => q) => ((All (x,p)) => q))) is valid by Th23, LUKASI_1:41; (All (x,((p => q) => ((All (x,p)) => q)))) => ((Ex (x,(p => q))) => (Ex (x,((All (x,p)) => q)))) is valid by Th34; then (Ex (x,(p => q))) => (Ex (x,((All (x,p)) => q))) is valid by A3, CQC_THE1:65; hence (Ex (x,(p => q))) => ((All (x,p)) => q) is valid by A2, LUKASI_1:42; ::_thesis: verum end; theorem Th78: :: CQC_THE2:78 for A being QC-alphabet for p, q being Element of CQC-WFF A for x being bound_QC-variable of A holds ((All (x,p)) => q) => (Ex (x,(p => q))) is valid proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A for x being bound_QC-variable of A holds ((All (x,p)) => q) => (Ex (x,(p => q))) is valid let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A holds ((All (x,p)) => q) => (Ex (x,(p => q))) is valid let x be bound_QC-variable of A; ::_thesis: ((All (x,p)) => q) => (Ex (x,(p => q))) is valid (All (x,(p '&' ('not' q)))) => ((All (x,p)) '&' ('not' q)) is valid by Th65; then ('not' ((All (x,p)) '&' ('not' q))) => ('not' (All (x,(p '&' ('not' q))))) is valid by LUKASI_1:52; then A1: ((All (x,p)) => q) => ('not' (All (x,(p '&' ('not' q))))) is valid by QC_LANG2:def_2; ( All (x,(('not' ('not' (p '&' ('not' q)))) => (p '&' ('not' q)))) is valid & (All (x,(('not' ('not' (p '&' ('not' q)))) => (p '&' ('not' q))))) => ((All (x,('not' ('not' (p '&' ('not' q)))))) => (All (x,(p '&' ('not' q))))) is valid ) by Th23, Th30; then (All (x,('not' ('not' (p '&' ('not' q)))))) => (All (x,(p '&' ('not' q)))) is valid by CQC_THE1:65; then ('not' (All (x,(p '&' ('not' q))))) => ('not' (All (x,('not' ('not' (p '&' ('not' q))))))) is valid by LUKASI_1:52; then ((All (x,p)) => q) => ('not' (All (x,('not' ('not' (p '&' ('not' q))))))) is valid by A1, LUKASI_1:42; then ((All (x,p)) => q) => (Ex (x,('not' (p '&' ('not' q))))) is valid by QC_LANG2:def_5; hence ((All (x,p)) => q) => (Ex (x,(p => q))) is valid by QC_LANG2:def_2; ::_thesis: verum end; theorem :: CQC_THE2:79 for A being QC-alphabet for q, p being Element of CQC-WFF A for x being bound_QC-variable of A st not x in still_not-bound_in q holds ( (All (x,p)) => q is valid iff Ex (x,(p => q)) is valid ) proof let A be QC-alphabet ; ::_thesis: for q, p being Element of CQC-WFF A for x being bound_QC-variable of A st not x in still_not-bound_in q holds ( (All (x,p)) => q is valid iff Ex (x,(p => q)) is valid ) let q, p be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A st not x in still_not-bound_in q holds ( (All (x,p)) => q is valid iff Ex (x,(p => q)) is valid ) let x be bound_QC-variable of A; ::_thesis: ( not x in still_not-bound_in q implies ( (All (x,p)) => q is valid iff Ex (x,(p => q)) is valid ) ) assume not x in still_not-bound_in q ; ::_thesis: ( (All (x,p)) => q is valid iff Ex (x,(p => q)) is valid ) then A1: (Ex (x,(p => q))) => ((All (x,p)) => q) is valid by Th77; ((All (x,p)) => q) => (Ex (x,(p => q))) is valid by Th78; then ((All (x,p)) => q) <=> (Ex (x,(p => q))) is valid by A1, Lm14; hence ( (All (x,p)) => q is valid iff Ex (x,(p => q)) is valid ) by Lm15; ::_thesis: verum end; theorem Th80: :: CQC_THE2:80 for A being QC-alphabet for q, p being Element of CQC-WFF A for x being bound_QC-variable of A st not x in still_not-bound_in q holds ( ((Ex (x,p)) => q) => (All (x,(p => q))) is valid & (All (x,(p => q))) => ((Ex (x,p)) => q) is valid ) proof let A be QC-alphabet ; ::_thesis: for q, p being Element of CQC-WFF A for x being bound_QC-variable of A st not x in still_not-bound_in q holds ( ((Ex (x,p)) => q) => (All (x,(p => q))) is valid & (All (x,(p => q))) => ((Ex (x,p)) => q) is valid ) let q, p be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A st not x in still_not-bound_in q holds ( ((Ex (x,p)) => q) => (All (x,(p => q))) is valid & (All (x,(p => q))) => ((Ex (x,p)) => q) is valid ) let x be bound_QC-variable of A; ::_thesis: ( not x in still_not-bound_in q implies ( ((Ex (x,p)) => q) => (All (x,(p => q))) is valid & (All (x,(p => q))) => ((Ex (x,p)) => q) is valid ) ) assume A1: not x in still_not-bound_in q ; ::_thesis: ( ((Ex (x,p)) => q) => (All (x,(p => q))) is valid & (All (x,(p => q))) => ((Ex (x,p)) => q) is valid ) p => (Ex (x,p)) is valid by Th15; then A2: ((Ex (x,p)) => q) => (p => q) is valid by LUKASI_1:41; not x in still_not-bound_in (Ex (x,p)) by Th6; then not x in still_not-bound_in ((Ex (x,p)) => q) by A1, Th7; hence ((Ex (x,p)) => q) => (All (x,(p => q))) is valid by A2, CQC_THE1:67; ::_thesis: (All (x,(p => q))) => ((Ex (x,p)) => q) is valid (All (x,(p => q))) => ((Ex (x,p)) => (Ex (x,q))) is valid by Th34; then A3: ((All (x,(p => q))) '&' (Ex (x,p))) => (Ex (x,q)) is valid by Th1; (Ex (x,q)) => q is valid by A1, Th20; then ((All (x,(p => q))) '&' (Ex (x,p))) => q is valid by A3, LUKASI_1:42; hence (All (x,(p => q))) => ((Ex (x,p)) => q) is valid by Th3; ::_thesis: verum end; theorem Th81: :: CQC_THE2:81 for A being QC-alphabet for q, p being Element of CQC-WFF A for x being bound_QC-variable of A st not x in still_not-bound_in q holds ((Ex (x,p)) => q) <=> (All (x,(p => q))) is valid proof let A be QC-alphabet ; ::_thesis: for q, p being Element of CQC-WFF A for x being bound_QC-variable of A st not x in still_not-bound_in q holds ((Ex (x,p)) => q) <=> (All (x,(p => q))) is valid let q, p be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A st not x in still_not-bound_in q holds ((Ex (x,p)) => q) <=> (All (x,(p => q))) is valid let x be bound_QC-variable of A; ::_thesis: ( not x in still_not-bound_in q implies ((Ex (x,p)) => q) <=> (All (x,(p => q))) is valid ) assume not x in still_not-bound_in q ; ::_thesis: ((Ex (x,p)) => q) <=> (All (x,(p => q))) is valid then ( ((Ex (x,p)) => q) => (All (x,(p => q))) is valid & (All (x,(p => q))) => ((Ex (x,p)) => q) is valid ) by Th80; hence ((Ex (x,p)) => q) <=> (All (x,(p => q))) is valid by Lm14; ::_thesis: verum end; theorem :: CQC_THE2:82 for A being QC-alphabet for q, p being Element of CQC-WFF A for x being bound_QC-variable of A st not x in still_not-bound_in q holds ( (Ex (x,p)) => q is valid iff All (x,(p => q)) is valid ) proof let A be QC-alphabet ; ::_thesis: for q, p being Element of CQC-WFF A for x being bound_QC-variable of A st not x in still_not-bound_in q holds ( (Ex (x,p)) => q is valid iff All (x,(p => q)) is valid ) let q, p be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A st not x in still_not-bound_in q holds ( (Ex (x,p)) => q is valid iff All (x,(p => q)) is valid ) let x be bound_QC-variable of A; ::_thesis: ( not x in still_not-bound_in q implies ( (Ex (x,p)) => q is valid iff All (x,(p => q)) is valid ) ) assume not x in still_not-bound_in q ; ::_thesis: ( (Ex (x,p)) => q is valid iff All (x,(p => q)) is valid ) then ((Ex (x,p)) => q) <=> (All (x,(p => q))) is valid by Th81; hence ( (Ex (x,p)) => q is valid iff All (x,(p => q)) is valid ) by Lm15; ::_thesis: verum end; theorem Th83: :: CQC_THE2:83 for A being QC-alphabet for p, q being Element of CQC-WFF A for x being bound_QC-variable of A st not x in still_not-bound_in p holds (Ex (x,(p => q))) => (p => (Ex (x,q))) is valid proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A for x being bound_QC-variable of A st not x in still_not-bound_in p holds (Ex (x,(p => q))) => (p => (Ex (x,q))) is valid let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A st not x in still_not-bound_in p holds (Ex (x,(p => q))) => (p => (Ex (x,q))) is valid let x be bound_QC-variable of A; ::_thesis: ( not x in still_not-bound_in p implies (Ex (x,(p => q))) => (p => (Ex (x,q))) is valid ) assume A1: not x in still_not-bound_in p ; ::_thesis: (Ex (x,(p => q))) => (p => (Ex (x,q))) is valid not x in still_not-bound_in (Ex (x,q)) by Th6; then not x in still_not-bound_in (p => (Ex (x,q))) by A1, Th7; then A2: (Ex (x,(p => (Ex (x,q))))) => (p => (Ex (x,q))) is valid by Th20; q => (Ex (x,q)) is valid by Th15; then A3: All (x,((p => q) => (p => (Ex (x,q))))) is valid by Th23, LUKASI_1:51; (All (x,((p => q) => (p => (Ex (x,q)))))) => ((Ex (x,(p => q))) => (Ex (x,(p => (Ex (x,q)))))) is valid by Th34; then (Ex (x,(p => q))) => (Ex (x,(p => (Ex (x,q))))) is valid by A3, CQC_THE1:65; hence (Ex (x,(p => q))) => (p => (Ex (x,q))) is valid by A2, LUKASI_1:42; ::_thesis: verum end; theorem Th84: :: CQC_THE2:84 for A being QC-alphabet for p, q being Element of CQC-WFF A for x being bound_QC-variable of A holds (p => (Ex (x,q))) => (Ex (x,(p => q))) is valid proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A for x being bound_QC-variable of A holds (p => (Ex (x,q))) => (Ex (x,(p => q))) is valid let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A holds (p => (Ex (x,q))) => (Ex (x,(p => q))) is valid let x be bound_QC-variable of A; ::_thesis: (p => (Ex (x,q))) => (Ex (x,(p => q))) is valid ( All (x,(('not' ('not' (p '&' ('not' q)))) => (p '&' ('not' q)))) is valid & (All (x,(('not' ('not' (p '&' ('not' q)))) => (p '&' ('not' q))))) => ((All (x,('not' ('not' (p '&' ('not' q)))))) => (All (x,(p '&' ('not' q))))) is valid ) by Th23, Th30; then (All (x,('not' ('not' (p '&' ('not' q)))))) => (All (x,(p '&' ('not' q)))) is valid by CQC_THE1:65; then A1: ('not' (All (x,(p '&' ('not' q))))) => ('not' (All (x,('not' ('not' (p '&' ('not' q))))))) is valid by LUKASI_1:52; (All (x,('not' q))) <=> ('not' (Ex (x,q))) is valid by Th54; then (All (x,('not' q))) => ('not' (Ex (x,q))) is valid by Lm14; then (p '&' (All (x,('not' q)))) => (p '&' ('not' (Ex (x,q)))) is valid by Lm9; then A2: ('not' (p '&' ('not' (Ex (x,q))))) => ('not' (p '&' (All (x,('not' q))))) is valid by LUKASI_1:52; (All (x,(p '&' ('not' q)))) => (p '&' (All (x,('not' q)))) is valid by Th64; then ('not' (p '&' (All (x,('not' q))))) => ('not' (All (x,(p '&' ('not' q))))) is valid by LUKASI_1:52; then ('not' (p '&' ('not' (Ex (x,q))))) => ('not' (All (x,(p '&' ('not' q))))) is valid by A2, LUKASI_1:42; then (p => (Ex (x,q))) => ('not' (All (x,(p '&' ('not' q))))) is valid by QC_LANG2:def_2; then (p => (Ex (x,q))) => ('not' (All (x,('not' ('not' (p '&' ('not' q))))))) is valid by A1, LUKASI_1:42; then (p => (Ex (x,q))) => ('not' (All (x,('not' (p => q))))) is valid by QC_LANG2:def_2; hence (p => (Ex (x,q))) => (Ex (x,(p => q))) is valid by QC_LANG2:def_5; ::_thesis: verum end; theorem Th85: :: CQC_THE2:85 for A being QC-alphabet for p, q being Element of CQC-WFF A for x being bound_QC-variable of A st not x in still_not-bound_in p holds (p => (Ex (x,q))) <=> (Ex (x,(p => q))) is valid proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A for x being bound_QC-variable of A st not x in still_not-bound_in p holds (p => (Ex (x,q))) <=> (Ex (x,(p => q))) is valid let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A st not x in still_not-bound_in p holds (p => (Ex (x,q))) <=> (Ex (x,(p => q))) is valid let x be bound_QC-variable of A; ::_thesis: ( not x in still_not-bound_in p implies (p => (Ex (x,q))) <=> (Ex (x,(p => q))) is valid ) assume not x in still_not-bound_in p ; ::_thesis: (p => (Ex (x,q))) <=> (Ex (x,(p => q))) is valid then A1: (Ex (x,(p => q))) => (p => (Ex (x,q))) is valid by Th83; (p => (Ex (x,q))) => (Ex (x,(p => q))) is valid by Th84; hence (p => (Ex (x,q))) <=> (Ex (x,(p => q))) is valid by A1, Lm14; ::_thesis: verum end; theorem :: CQC_THE2:86 for A being QC-alphabet for p, q being Element of CQC-WFF A for x being bound_QC-variable of A st not x in still_not-bound_in p holds ( p => (Ex (x,q)) is valid iff Ex (x,(p => q)) is valid ) proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A for x being bound_QC-variable of A st not x in still_not-bound_in p holds ( p => (Ex (x,q)) is valid iff Ex (x,(p => q)) is valid ) let p, q be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A st not x in still_not-bound_in p holds ( p => (Ex (x,q)) is valid iff Ex (x,(p => q)) is valid ) let x be bound_QC-variable of A; ::_thesis: ( not x in still_not-bound_in p implies ( p => (Ex (x,q)) is valid iff Ex (x,(p => q)) is valid ) ) assume not x in still_not-bound_in p ; ::_thesis: ( p => (Ex (x,q)) is valid iff Ex (x,(p => q)) is valid ) then (p => (Ex (x,q))) <=> (Ex (x,(p => q))) is valid by Th85; hence ( p => (Ex (x,q)) is valid iff Ex (x,(p => q)) is valid ) by Lm15; ::_thesis: verum end; theorem :: CQC_THE2:87 for A being QC-alphabet for p being Element of CQC-WFF A holds {p} |- p proof let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A holds {p} |- p let p be Element of CQC-WFF A; ::_thesis: {p} |- p ( p in {p} & {p} c= Cn {p} ) by CQC_THE1:17, TARSKI:def_1; hence p in Cn {p} ; :: according to CQC_THE1:def_8 ::_thesis: verum end; theorem Th88: :: CQC_THE2:88 for A being QC-alphabet for p, q being Element of CQC-WFF A holds Cn ({p} \/ {q}) = Cn {(p '&' q)} proof let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds Cn ({p} \/ {q}) = Cn {(p '&' q)} let p, q be Element of CQC-WFF A; ::_thesis: Cn ({p} \/ {q}) = Cn {(p '&' q)} for t being Element of CQC-WFF A holds ( t in Cn ({p} \/ {q}) iff for T being Subset of (CQC-WFF A) st T is being_a_theory & {(p '&' q)} c= T holds t in T ) proof let t be Element of CQC-WFF A; ::_thesis: ( t in Cn ({p} \/ {q}) iff for T being Subset of (CQC-WFF A) st T is being_a_theory & {(p '&' q)} c= T holds t in T ) thus ( t in Cn ({p} \/ {q}) implies for T being Subset of (CQC-WFF A) st T is being_a_theory & {(p '&' q)} c= T holds t in T ) ::_thesis: ( ( for T being Subset of (CQC-WFF A) st T is being_a_theory & {(p '&' q)} c= T holds t in T ) implies t in Cn ({p} \/ {q}) ) proof assume A1: t in Cn ({p} \/ {q}) ; ::_thesis: for T being Subset of (CQC-WFF A) st T is being_a_theory & {(p '&' q)} c= T holds t in T let T be Subset of (CQC-WFF A); ::_thesis: ( T is being_a_theory & {(p '&' q)} c= T implies t in T ) assume that A2: T is being_a_theory and A3: {(p '&' q)} c= T ; ::_thesis: t in T A4: ( p '&' q in T & TAUT A c= T ) by A2, A3, CQC_THE1:38, ZFMISC_1:31; (p '&' q) => q in TAUT A by PROCAL_1:21; then q in T by A2, A4, CQC_THE1:def_1; then A5: {q} c= T by ZFMISC_1:31; (p '&' q) => p in TAUT A by PROCAL_1:19; then p in T by A2, A4, CQC_THE1:def_1; then {p} c= T by ZFMISC_1:31; then {p} \/ {q} c= T by A5, XBOOLE_1:8; hence t in T by A1, A2, CQC_THE1:def_2; ::_thesis: verum end; thus ( ( for T being Subset of (CQC-WFF A) st T is being_a_theory & {(p '&' q)} c= T holds t in T ) implies t in Cn ({p} \/ {q}) ) ::_thesis: verum proof assume A6: for T being Subset of (CQC-WFF A) st T is being_a_theory & {(p '&' q)} c= T holds t in T ; ::_thesis: t in Cn ({p} \/ {q}) for T being Subset of (CQC-WFF A) st T is being_a_theory & {p} \/ {q} c= T holds t in T proof let T be Subset of (CQC-WFF A); ::_thesis: ( T is being_a_theory & {p} \/ {q} c= T implies t in T ) assume that A7: T is being_a_theory and A8: {p} \/ {q} c= T ; ::_thesis: t in T {p} c= {p} \/ {q} by XBOOLE_1:7; then {p} c= T by A8, XBOOLE_1:1; then A9: p in T by ZFMISC_1:31; {q} c= {p} \/ {q} by XBOOLE_1:7; then {q} c= T by A8, XBOOLE_1:1; then A10: q in T by ZFMISC_1:31; ( p => (q => (p '&' q)) in TAUT A & TAUT A c= T ) by A7, CQC_THE1:38, PROCAL_1:28; then q => (p '&' q) in T by A7, A9, CQC_THE1:def_1; then p '&' q in T by A7, A10, CQC_THE1:def_1; then {(p '&' q)} c= T by ZFMISC_1:31; hence t in T by A6, A7; ::_thesis: verum end; hence t in Cn ({p} \/ {q}) by CQC_THE1:def_2; ::_thesis: verum end; end; hence Cn ({p} \/ {q}) = Cn {(p '&' q)} by CQC_THE1:def_2; ::_thesis: verum end; theorem :: CQC_THE2:89 for A being QC-alphabet for p, q, r being Element of CQC-WFF A holds ( {p,q} |- r iff {(p '&' q)} |- r ) proof let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A holds ( {p,q} |- r iff {(p '&' q)} |- r ) let p, q, r be Element of CQC-WFF A; ::_thesis: ( {p,q} |- r iff {(p '&' q)} |- r ) thus ( {p,q} |- r implies {(p '&' q)} |- r ) ::_thesis: ( {(p '&' q)} |- r implies {p,q} |- r ) proof assume r in Cn {p,q} ; :: according to CQC_THE1:def_8 ::_thesis: {(p '&' q)} |- r then r in Cn ({p} \/ {q}) by ENUMSET1:1; hence r in Cn {(p '&' q)} by Th88; :: according to CQC_THE1:def_8 ::_thesis: verum end; assume r in Cn {(p '&' q)} ; :: according to CQC_THE1:def_8 ::_thesis: {p,q} |- r then r in Cn ({p} \/ {q}) by Th88; hence r in Cn {p,q} by ENUMSET1:1; :: according to CQC_THE1:def_8 ::_thesis: verum end; theorem Th90: :: CQC_THE2:90 for A being QC-alphabet for X being Subset of (CQC-WFF A) for p being Element of CQC-WFF A for x being bound_QC-variable of A st X |- p holds X |- All (x,p) proof let A be QC-alphabet ; ::_thesis: for X being Subset of (CQC-WFF A) for p being Element of CQC-WFF A for x being bound_QC-variable of A st X |- p holds X |- All (x,p) let X be Subset of (CQC-WFF A); ::_thesis: for p being Element of CQC-WFF A for x being bound_QC-variable of A st X |- p holds X |- All (x,p) let p be Element of CQC-WFF A; ::_thesis: for x being bound_QC-variable of A st X |- p holds X |- All (x,p) let x be bound_QC-variable of A; ::_thesis: ( X |- p implies X |- All (x,p) ) A1: X |- p => (((All (x,p)) => (All (x,p))) => p) by CQC_THE1:59; not x in still_not-bound_in (All (x,p)) by Th5; then A2: not x in still_not-bound_in ((All (x,p)) => (All (x,p))) by Th7; assume X |- p ; ::_thesis: X |- All (x,p) then X |- ((All (x,p)) => (All (x,p))) => p by A1, CQC_THE1:55; then A3: X |- ((All (x,p)) => (All (x,p))) => (All (x,p)) by A2, CQC_THE1:57; X |- (All (x,p)) => (All (x,p)) by CQC_THE1:59; hence X |- All (x,p) by A3, CQC_THE1:55; ::_thesis: verum end; theorem :: CQC_THE2:91 for A being QC-alphabet for X being Subset of (CQC-WFF A) for p, q being Element of CQC-WFF A for x being bound_QC-variable of A st not x in still_not-bound_in p holds X |- (All (x,(p => q))) => (p => (All (x,q))) by Th74, CQC_THE1:59; theorem :: CQC_THE2:92 for A being QC-alphabet for X being Subset of (CQC-WFF A) for F, G being Element of CQC-WFF A st F is closed & X \/ {F} |- G holds X |- F => G proof let A be QC-alphabet ; ::_thesis: for X being Subset of (CQC-WFF A) for F, G being Element of CQC-WFF A st F is closed & X \/ {F} |- G holds X |- F => G let X be Subset of (CQC-WFF A); ::_thesis: for F, G being Element of CQC-WFF A st F is closed & X \/ {F} |- G holds X |- F => G let F, G be Element of CQC-WFF A; ::_thesis: ( F is closed & X \/ {F} |- G implies X |- F => G ) assume that A1: F is closed and A2: X \/ {F} |- G ; ::_thesis: X |- F => G G in Cn (X \/ {F}) by A2, CQC_THE1:def_8; then consider f being FinSequence of [:(CQC-WFF A),Proof_Step_Kinds:] such that A3: f is_a_proof_wrt X \/ {F} and A4: Effect f = G by CQC_THE1:36; f <> {} by A3, CQC_THE1:def_5; then A5: G = (f . (len f)) `1 by A4, CQC_THE1:def_6; defpred S1[ Nat] means ( 1 <= \$1 & \$1 <= len f implies for H being Element of CQC-WFF A st H = (f . \$1) `1 holds X |- F => H ); A6: for n being Nat st ( for k being Nat st k < n holds S1[k] ) holds S1[n] proof let n be Nat; ::_thesis: ( ( for k being Nat st k < n holds S1[k] ) implies S1[n] ) assume A7: for k being Nat st k < n & 1 <= k & k <= len f holds for H being Element of CQC-WFF A st H = (f . k) `1 holds X |- F => H ; ::_thesis: S1[n] assume that A8: 1 <= n and A9: n <= len f ; ::_thesis: for H being Element of CQC-WFF A st H = (f . n) `1 holds X |- F => H n in NAT by ORDINAL1:def_12; then A10: f,n is_a_correct_step_wrt X \/ {F} by A3, A8, A9, CQC_THE1:def_5; let H be Element of CQC-WFF A; ::_thesis: ( H = (f . n) `1 implies X |- F => H ) assume A11: H = (f . n) `1 ; ::_thesis: X |- F => H now__::_thesis:_X_|-_F_=>_H percases ( (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 A8, A9, CQC_THE1:23; suppose (f . n) `2 = 0 ; ::_thesis: X |- F => H then H in X \/ {F} by A11, A10, CQC_THE1:def_4; then A12: ( H in X or H in {F} ) by XBOOLE_0:def_3; now__::_thesis:_X_|-_F_=>_H percases ( H in X or H = F ) by A12, TARSKI:def_1; supposeA13: H in X ; ::_thesis: X |- F => H X c= Cn X by CQC_THE1:17; then A14: X |- H by A13, CQC_THE1:def_8; X |- H => (F => H) by CQC_THE1:59; hence X |- F => H by A14, CQC_THE1:55; ::_thesis: verum end; suppose H = F ; ::_thesis: X |- F => H hence X |- F => H by CQC_THE1:59; ::_thesis: verum end; end; end; hence X |- F => H ; ::_thesis: verum end; suppose (f . n) `2 = 1 ; ::_thesis: X |- F => H then H = VERUM A by A11, A10, CQC_THE1:def_4; hence X |- F => H by CQC_THE1:59, LUKASI_1:46; ::_thesis: verum end; suppose (f . n) `2 = 2 ; ::_thesis: X |- F => H then ex p being Element of CQC-WFF A st H = (('not' p) => p) => p by A11, A10, CQC_THE1:def_4; then H is valid by CQC_THE1:61; hence X |- F => H by CQC_THE1:59, LUKASI_1:61; ::_thesis: verum end; suppose (f . n) `2 = 3 ; ::_thesis: X |- F => H then ex p, q being Element of CQC-WFF A st H = p => (('not' p) => q) by A11, A10, CQC_THE1:def_4; then H is valid by CQC_THE1:62; hence X |- F => H by CQC_THE1:59, LUKASI_1:61; ::_thesis: verum end; suppose (f . n) `2 = 4 ; ::_thesis: X |- F => H then ex p, q, r being Element of CQC-WFF A st H = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) by A11, A10, CQC_THE1:def_4; then H is valid by CQC_THE1:63; hence X |- F => H by CQC_THE1:59, LUKASI_1:61; ::_thesis: verum end; suppose (f . n) `2 = 5 ; ::_thesis: X |- F => H then ex p, q being Element of CQC-WFF A st H = (p '&' q) => (q '&' p) by A11, A10, CQC_THE1:def_4; then H is valid by CQC_THE1:64; hence X |- F => H by CQC_THE1:59, LUKASI_1:61; ::_thesis: verum end; suppose (f . n) `2 = 6 ; ::_thesis: X |- F => H then ex p being Element of CQC-WFF A ex x being bound_QC-variable of A st H = (All (x,p)) => p by A11, A10, CQC_THE1:def_4; then H is valid by CQC_THE1:66; hence X |- F => H by CQC_THE1:59, LUKASI_1:61; ::_thesis: verum end; suppose (f . n) `2 = 7 ; ::_thesis: X |- F => H then consider i, j being Element of NAT , p, q being Element of CQC-WFF A such that A15: 1 <= i and A16: i < n and A17: 1 <= j and A18: j < i and A19: p = (f . j) `1 and A20: q = H and A21: (f . i) `1 = p => q by A11, A10, CQC_THE1:def_4; i <= len f by A9, A16, XXREAL_0:2; then A22: X |- F => (p => q) by A7, A15, A16, A21; X |- (F => (p => q)) => ((F => p) => (F => q)) by CQC_THE1:59; then A23: X |- (F => p) => (F => q) by A22, CQC_THE1:55; j < n by A16, A18, XXREAL_0:2; then A24: j <= len f by A9, XXREAL_0:2; j < n by A16, A18, XXREAL_0:2; then X |- F => p by A7, A17, A19, A24; hence X |- F => H by A20, A23, CQC_THE1:55; ::_thesis: verum end; suppose (f . n) `2 = 8 ; ::_thesis: X |- F => H then consider i being Element of NAT , p, q being Element of CQC-WFF A, x being bound_QC-variable of A such that A25: 1 <= i and A26: i < n and A27: (f . i) `1 = p => q and A28: not x in still_not-bound_in p and A29: H = p => (All (x,q)) by A11, A10, CQC_THE1:def_4; A30: X |- (All (x,(p => q))) => (p => (All (x,q))) by A28, Th74, CQC_THE1:59; not x in still_not-bound_in F by A1, QC_LANG1:def_31; then A31: X |- (All (x,(F => (p => q)))) => (F => (All (x,(p => q)))) by Th74, CQC_THE1:59; i <= len f by A9, A26, XXREAL_0:2; then X |- All (x,(F => (p => q))) by A7, A25, A26, A27, Th90; then X |- F => (All (x,(p => q))) by A31, CQC_THE1:55; hence X |- F => H by A29, A30, LUKASI_1:59; ::_thesis: verum end; suppose (f . n) `2 = 9 ; ::_thesis: X |- F => H then consider i being Element of NAT , x, y being bound_QC-variable of A, s being QC-formula of A such that A32: 1 <= i and A33: i < n and A34: ( s . x in CQC-WFF A & s . y in CQC-WFF A ) and A35: not x in still_not-bound_in s and A36: s . x = (f . i) `1 and A37: H = s . y by A11, A10, CQC_THE1:def_4; reconsider s1 = s . x, s2 = s . y as Element of CQC-WFF A by A34; A38: X |- (All (x,s1)) => s2 by A35, Th25, CQC_THE1:59; not x in still_not-bound_in F by A1, QC_LANG1:def_31; then A39: X |- (All (x,(F => s1))) => (F => (All (x,s1))) by Th74, CQC_THE1:59; i <= len f by A9, A33, XXREAL_0:2; then X |- All (x,(F => s1)) by A7, A32, A33, A36, Th90; then X |- F => (All (x,s1)) by A39, CQC_THE1:55; hence X |- F => H by A37, A38, LUKASI_1:59; ::_thesis: verum end; end; end; hence X |- F => H ; ::_thesis: verum end; A40: for n being Nat holds S1[n] from NAT_1:sch_4(A6); 1 <= len f by A3, CQC_THE1:25; hence X |- F => G by A40, A5; ::_thesis: verum end;