:: LUKASI_1  semantic presentation begin  













theorem :: LUKASI_1:1 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A"))) "holds"  (Bool (Set (Set  "(" (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "q")) ")" )  ($#k8_cqc_lang :::"=>"::: )  (Set  "(" (Set  "(" (Set (Var "q"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "r")) ")" )  ($#k8_cqc_lang :::"=>"::: )  (Set  "(" (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "r")) ")" ) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_cqc_the1 :::"TAUT"::: )  (Set (Var "A")))))) ; 
 
theorem :: LUKASI_1:2 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A")))  "st" (Bool (Bool (Set (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "q")))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_cqc_the1 :::"TAUT"::: )  (Set (Var "A"))))) "holds"  (Bool (Set (Set  "(" (Set (Var "q"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "r")) ")" )  ($#k8_cqc_lang :::"=>"::: )  (Set  "(" (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "r")) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_cqc_the1 :::"TAUT"::: )  (Set (Var "A")))))) ; 
 
theorem :: LUKASI_1:3 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A")))  "st" (Bool (Bool (Set (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "q")))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_cqc_the1 :::"TAUT"::: )  (Set (Var "A")))) & (Bool (Set (Set (Var "q"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "r")))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_cqc_the1 :::"TAUT"::: )  (Set (Var "A"))))) "holds"  (Bool (Set (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "r")))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_cqc_the1 :::"TAUT"::: )  (Set (Var "A")))))) ; 
 
theorem :: LUKASI_1:4 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "p")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A"))) "holds"  (Bool (Set (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "p")))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_cqc_the1 :::"TAUT"::: )  (Set (Var "A")))))) ; 
 
theorem :: LUKASI_1:5 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "q")) "," (Set (Var "p")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A"))) "holds"  (Bool (Set (Set (Var "q"))  ($#k8_cqc_lang :::"=>"::: )  (Set  "(" (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "q")) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_cqc_the1 :::"TAUT"::: )  (Set (Var "A")))))) ; 
 
theorem :: LUKASI_1:6 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A"))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "q")) ")" )  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "r")) ")" )  ($#k8_cqc_lang :::"=>"::: )  (Set  "(" (Set (Var "q"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "r")) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_cqc_the1 :::"TAUT"::: )  (Set (Var "A")))))) ; 
 
theorem :: LUKASI_1:7 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "q")) "," (Set (Var "p")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A"))) "holds"  (Bool (Set (Set (Var "q"))  ($#k8_cqc_lang :::"=>"::: )  (Set  "(" (Set  "(" (Set (Var "q"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "p")) ")" )  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "p")) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_cqc_the1 :::"TAUT"::: )  (Set (Var "A")))))) ; 
 
theorem :: LUKASI_1:8 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "s")) "," (Set (Var "q")) "," (Set (Var "p")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A"))) "holds"  (Bool (Set (Set  "(" (Set (Var "s"))  ($#k8_cqc_lang :::"=>"::: )  (Set  "(" (Set (Var "q"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "p")) ")" ) ")" )  ($#k8_cqc_lang :::"=>"::: )  (Set  "(" (Set (Var "q"))  ($#k8_cqc_lang :::"=>"::: )  (Set  "(" (Set (Var "s"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "p")) ")" ) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_cqc_the1 :::"TAUT"::: )  (Set (Var "A")))))) ; 
 
theorem :: LUKASI_1:9 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "p")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A"))) "holds"  (Bool (Set (Set  "(" (Set (Var "q"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "r")) ")" )  ($#k8_cqc_lang :::"=>"::: )  (Set  "(" (Set  "(" (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "q")) ")" )  ($#k8_cqc_lang :::"=>"::: )  (Set  "(" (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "r")) ")" ) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_cqc_the1 :::"TAUT"::: )  (Set (Var "A")))))) ; 
 
theorem :: LUKASI_1:10 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "q")) "," (Set (Var "r")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A"))) "holds"  (Bool (Set (Set  "(" (Set (Var "q"))  ($#k8_cqc_lang :::"=>"::: )  (Set  "(" (Set (Var "q"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "r")) ")" ) ")" )  ($#k8_cqc_lang :::"=>"::: )  (Set  "(" (Set (Var "q"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "r")) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_cqc_the1 :::"TAUT"::: )  (Set (Var "A")))))) ; 
 
theorem :: LUKASI_1:11 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A"))) "holds"  (Bool (Set (Set  "(" (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set  "(" (Set (Var "q"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "r")) ")" ) ")" )  ($#k8_cqc_lang :::"=>"::: )  (Set  "(" (Set  "(" (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "q")) ")" )  ($#k8_cqc_lang :::"=>"::: )  (Set  "(" (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "r")) ")" ) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_cqc_the1 :::"TAUT"::: )  (Set (Var "A")))))) ; 
 
theorem :: LUKASI_1:12 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "p")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A"))) "holds"  (Bool (Set (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set  "("  ($#k5_cqc_lang :::"VERUM"::: )  (Set (Var "A")) ")" ) ")" )  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "p")))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_cqc_the1 :::"TAUT"::: )  (Set (Var "A")))))) ; 
 
theorem :: LUKASI_1:13 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "q")) "," (Set (Var "p")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A")))  "st" (Bool (Bool (Set (Var "q"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_cqc_the1 :::"TAUT"::: )  (Set (Var "A"))))) "holds"  (Bool (Set (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "q")))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_cqc_the1 :::"TAUT"::: )  (Set (Var "A")))))) ; 
 
theorem :: LUKASI_1:14 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A")))  "st" (Bool (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_cqc_the1 :::"TAUT"::: )  (Set (Var "A"))))) "holds"  (Bool (Set (Set  "(" (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "q")) ")" )  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "q")))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_cqc_the1 :::"TAUT"::: )  (Set (Var "A")))))) ; 
 
theorem :: LUKASI_1:15 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "s")) "," (Set (Var "q")) "," (Set (Var "p")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A")))  "st" (Bool (Bool (Set (Set (Var "s"))  ($#k8_cqc_lang :::"=>"::: )  (Set  "(" (Set (Var "q"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "p")) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_cqc_the1 :::"TAUT"::: )  (Set (Var "A"))))) "holds"  (Bool (Set (Set (Var "q"))  ($#k8_cqc_lang :::"=>"::: )  (Set  "(" (Set (Var "s"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "p")) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_cqc_the1 :::"TAUT"::: )  (Set (Var "A")))))) ; 
 
theorem :: LUKASI_1:16 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "s")) "," (Set (Var "q")) "," (Set (Var "p")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A")))  "st" (Bool (Bool (Set (Set (Var "s"))  ($#k8_cqc_lang :::"=>"::: )  (Set  "(" (Set (Var "q"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "p")) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_cqc_the1 :::"TAUT"::: )  (Set (Var "A")))) & (Bool (Set (Var "q"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_cqc_the1 :::"TAUT"::: )  (Set (Var "A"))))) "holds"  (Bool (Set (Set (Var "s"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "p")))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_cqc_the1 :::"TAUT"::: )  (Set (Var "A")))))) ; 
 
theorem :: LUKASI_1:17 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "s")) "," (Set (Var "q")) "," (Set (Var "p")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A")))  "st" (Bool (Bool (Set (Set (Var "s"))  ($#k8_cqc_lang :::"=>"::: )  (Set  "(" (Set (Var "q"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "p")) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_cqc_the1 :::"TAUT"::: )  (Set (Var "A")))) & (Bool (Set (Var "q"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_cqc_the1 :::"TAUT"::: )  (Set (Var "A")))) & (Bool (Set (Var "s"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_cqc_the1 :::"TAUT"::: )  (Set (Var "A"))))) "holds"  (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_cqc_the1 :::"TAUT"::: )  (Set (Var "A")))))) ; 
 
theorem :: LUKASI_1:18 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "q")) "," (Set (Var "r")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A")))  "st" (Bool (Bool (Set (Set (Var "q"))  ($#k8_cqc_lang :::"=>"::: )  (Set  "(" (Set (Var "q"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "r")) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_cqc_the1 :::"TAUT"::: )  (Set (Var "A"))))) "holds"  (Bool (Set (Set (Var "q"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "r")))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_cqc_the1 :::"TAUT"::: )  (Set (Var "A")))))) ; 
 
theorem :: LUKASI_1:19 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A")))  "st" (Bool (Bool (Set (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set  "(" (Set (Var "q"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "r")) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_cqc_the1 :::"TAUT"::: )  (Set (Var "A"))))) "holds"  (Bool (Set (Set  "(" (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "q")) ")" )  ($#k8_cqc_lang :::"=>"::: )  (Set  "(" (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "r")) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_cqc_the1 :::"TAUT"::: )  (Set (Var "A")))))) ; 
 
theorem :: LUKASI_1:20 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A")))  "st" (Bool (Bool (Set (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set  "(" (Set (Var "q"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "r")) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_cqc_the1 :::"TAUT"::: )  (Set (Var "A")))) & (Bool (Set (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "q")))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_cqc_the1 :::"TAUT"::: )  (Set (Var "A"))))) "holds"  (Bool (Set (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "r")))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_cqc_the1 :::"TAUT"::: )  (Set (Var "A")))))) ; 
 
theorem :: LUKASI_1:21 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A")))  "st" (Bool (Bool (Set (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set  "(" (Set (Var "q"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "r")) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_cqc_the1 :::"TAUT"::: )  (Set (Var "A")))) & (Bool (Set (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "q")))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_cqc_the1 :::"TAUT"::: )  (Set (Var "A")))) & (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_cqc_the1 :::"TAUT"::: )  (Set (Var "A"))))) "holds"  (Bool (Set (Var "r"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_cqc_the1 :::"TAUT"::: )  (Set (Var "A")))))) ; 
 
theorem :: LUKASI_1:22 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A")))  "st" (Bool (Bool (Set (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set  "(" (Set (Var "q"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "r")) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_cqc_the1 :::"TAUT"::: )  (Set (Var "A")))) & (Bool (Set (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set  "(" (Set (Var "r"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "s")) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_cqc_the1 :::"TAUT"::: )  (Set (Var "A"))))) "holds"  (Bool (Set (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set  "(" (Set (Var "q"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "s")) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_cqc_the1 :::"TAUT"::: )  (Set (Var "A")))))) ; 
 
theorem :: LUKASI_1:23 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "p")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A"))) "holds"  (Bool (Set (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set  "("  ($#k5_cqc_lang :::"VERUM"::: )  (Set (Var "A")) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_cqc_the1 :::"TAUT"::: )  (Set (Var "A")))))) ; 
 
theorem :: LUKASI_1:24 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A"))) "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k8_cqc_lang :::"=>"::: )  (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set (Var "q")) ")" ) ")" )  ($#k8_cqc_lang :::"=>"::: )  (Set  "(" (Set (Var "q"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "p")) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_cqc_the1 :::"TAUT"::: )  (Set (Var "A")))))) ; 
 
theorem :: LUKASI_1:25 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "p")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A"))) "holds"  (Bool (Set (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set (Var "p")) ")" ) ")" )  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "p")))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_cqc_the1 :::"TAUT"::: )  (Set (Var "A")))))) ; 
 
theorem :: LUKASI_1:26 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A"))) "holds"  (Bool (Set (Set  "(" (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "q")) ")" )  ($#k8_cqc_lang :::"=>"::: )  (Set  "(" (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set (Var "q")) ")" )  ($#k8_cqc_lang :::"=>"::: )  (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set (Var "p")) ")" ) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_cqc_the1 :::"TAUT"::: )  (Set (Var "A")))))) ; 
 
theorem :: LUKASI_1:27 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "p")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A"))) "holds"  (Bool (Set (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set (Var "p")) ")" ) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_cqc_the1 :::"TAUT"::: )  (Set (Var "A")))))) ; 
 
theorem :: LUKASI_1:28 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A"))) "holds"   (Bool  "("  (Bool (Set (Set  "(" (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set (Var "p")) ")" ) ")" )  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "q")) ")" )  ($#k8_cqc_lang :::"=>"::: )  (Set  "(" (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "q")) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_cqc_the1 :::"TAUT"::: )  (Set (Var "A")))) & (Bool (Set (Set  "(" (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "q")) ")" )  ($#k8_cqc_lang :::"=>"::: )  (Set  "(" (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set (Var "p")) ")" ) ")" )  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "q")) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_cqc_the1 :::"TAUT"::: )  (Set (Var "A"))))  ")" ))) ; 
 
theorem :: LUKASI_1:29 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A"))) "holds"   (Bool  "("  (Bool (Set (Set  "(" (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set (Var "q")) ")" ) ")" ) ")" )  ($#k8_cqc_lang :::"=>"::: )  (Set  "(" (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "q")) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_cqc_the1 :::"TAUT"::: )  (Set (Var "A")))) & (Bool (Set (Set  "(" (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "q")) ")" )  ($#k8_cqc_lang :::"=>"::: )  (Set  "(" (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set (Var "q")) ")" ) ")" ) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_cqc_the1 :::"TAUT"::: )  (Set (Var "A"))))  ")" ))) ; 
 
theorem :: LUKASI_1:30 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A"))) "holds"  (Bool (Set (Set  "(" (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set (Var "q")) ")" ) ")" )  ($#k8_cqc_lang :::"=>"::: )  (Set  "(" (Set (Var "q"))  ($#k8_cqc_lang :::"=>"::: )  (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set (Var "p")) ")" ) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_cqc_the1 :::"TAUT"::: )  (Set (Var "A")))))) ; 
 
theorem :: LUKASI_1:31 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A"))) "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "q")) ")" )  ($#k8_cqc_lang :::"=>"::: )  (Set  "(" (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set (Var "q")) ")" )  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "p")) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_cqc_the1 :::"TAUT"::: )  (Set (Var "A")))))) ; 
 
theorem :: LUKASI_1:32 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "p")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A"))) "holds"  (Bool (Set (Set  "(" (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set (Var "p")) ")" ) ")" )  ($#k8_cqc_lang :::"=>"::: )  (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set (Var "p")) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_cqc_the1 :::"TAUT"::: )  (Set (Var "A")))))) ; 
 
theorem :: LUKASI_1:33 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A"))) "holds"  (Bool (Set (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k8_cqc_lang :::"=>"::: )  (Set  "(" (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "q")) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_cqc_the1 :::"TAUT"::: )  (Set (Var "A")))))) ; 
 
theorem :: LUKASI_1:34 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A"))) "holds"   (Bool  "("  (Bool (Set (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "q")))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_cqc_the1 :::"TAUT"::: )  (Set (Var "A")))) "iff" (Bool (Set (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set (Var "q")) ")" )  ($#k8_cqc_lang :::"=>"::: )  (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set (Var "p")) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_cqc_the1 :::"TAUT"::: )  (Set (Var "A"))))  ")" ))) ; 
 
theorem :: LUKASI_1:35 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A")))  "st" (Bool (Bool (Set (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k8_cqc_lang :::"=>"::: )  (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set (Var "q")) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_cqc_the1 :::"TAUT"::: )  (Set (Var "A"))))) "holds"  (Bool (Set (Set (Var "q"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "p")))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_cqc_the1 :::"TAUT"::: )  (Set (Var "A")))))) ; 
 
theorem :: LUKASI_1:36 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "p")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A"))) "holds"   (Bool  "("  (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_cqc_the1 :::"TAUT"::: )  (Set (Var "A")))) "iff" (Bool (Set   ($#k6_cqc_lang :::"'not'"::: )  (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set (Var "p")) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_cqc_the1 :::"TAUT"::: )  (Set (Var "A"))))  ")" ))) ; 
 
theorem :: LUKASI_1:37 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A"))) "holds"   (Bool  "("  (Bool (Set (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "q")))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_cqc_the1 :::"TAUT"::: )  (Set (Var "A")))) "iff" (Bool (Set (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set (Var "q")) ")" ) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_cqc_the1 :::"TAUT"::: )  (Set (Var "A"))))  ")" ))) ; 
 
theorem :: LUKASI_1:38 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A"))) "holds"   (Bool  "("  (Bool (Set (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "q")))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_cqc_the1 :::"TAUT"::: )  (Set (Var "A")))) "iff" (Bool (Set (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set (Var "p")) ")" ) ")" )  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "q")))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_cqc_the1 :::"TAUT"::: )  (Set (Var "A"))))  ")" ))) ; 
 
theorem :: LUKASI_1:39 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A")))  "st" (Bool (Bool (Set (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set (Var "q")) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_cqc_the1 :::"TAUT"::: )  (Set (Var "A"))))) "holds"  (Bool (Set (Set (Var "q"))  ($#k8_cqc_lang :::"=>"::: )  (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set (Var "p")) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_cqc_the1 :::"TAUT"::: )  (Set (Var "A")))))) ; 
 
theorem :: LUKASI_1:40 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A")))  "st" (Bool (Bool (Set (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "q")))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_cqc_the1 :::"TAUT"::: )  (Set (Var "A"))))) "holds"  (Bool (Set (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set (Var "q")) ")" )  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "p")))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_cqc_the1 :::"TAUT"::: )  (Set (Var "A")))))) ; 
 registrationlet "A" be    ($#m1_qc_lang1 :::"QC-alphabet"::: )  ; let "p", "q", "r" be    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Const "A"))); 
cluster (Set bbbadK2_QC_LANG2("A" "," (Set  "(" "p"  ($#k8_cqc_lang :::"=>"::: )  "q" ")" ) "," (Set  "(" (Set  "(" "q"  ($#k8_cqc_lang :::"=>"::: )  "r" ")" )  ($#k8_cqc_lang :::"=>"::: )  (Set  "(" "p"  ($#k8_cqc_lang :::"=>"::: )  "r" ")" ) ")" ))) ->   ($#v2_cqc_the1 :::"valid"::: )   ; 
end; 
theorem :: LUKASI_1:41 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A")))  "st" (Bool (Bool (Set (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "q"))) "is"   ($#v2_cqc_the1 :::"valid"::: )  )) "holds"  (Bool (Set (Set  "(" (Set (Var "q"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "r")) ")" )  ($#k8_cqc_lang :::"=>"::: )  (Set  "(" (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "r")) ")" )) "is"   ($#v2_cqc_the1 :::"valid"::: )  ))) ; 
 
theorem :: LUKASI_1:42 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A")))  "st" (Bool (Bool (Set (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "q"))) "is"   ($#v2_cqc_the1 :::"valid"::: )  ) & (Bool (Set (Set (Var "q"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "r"))) "is"   ($#v2_cqc_the1 :::"valid"::: )  )) "holds"  (Bool (Set (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "r"))) "is"   ($#v2_cqc_the1 :::"valid"::: )  ))) ; 
 registrationlet "A" be    ($#m1_qc_lang1 :::"QC-alphabet"::: )  ; let "p" be    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Const "A"))); 
cluster (Set bbbadK2_QC_LANG2("A" "," "p" "," "p")) ->   ($#v2_cqc_the1 :::"valid"::: )   ; 
end; registrationlet "A" be    ($#m1_qc_lang1 :::"QC-alphabet"::: )  ; let "p", "q" be    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Const "A"))); 
cluster (Set bbbadK2_QC_LANG2("A" "," "p" "," (Set  "(" "q"  ($#k8_cqc_lang :::"=>"::: )  "p" ")" ))) ->   ($#v2_cqc_the1 :::"valid"::: )   ; 
end; 
theorem :: LUKASI_1:43 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A")))  "st" (Bool (Bool (Set (Var "p")) "is"   ($#v2_cqc_the1 :::"valid"::: )  )) "holds"  (Bool (Set (Set (Var "q"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "p"))) "is"   ($#v2_cqc_the1 :::"valid"::: )  ))) ; 
 registrationlet "A" be    ($#m1_qc_lang1 :::"QC-alphabet"::: )  ; let "p", "q", "s" be    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Const "A"))); 
cluster (Set bbbadK2_QC_LANG2("A" "," (Set  "(" "s"  ($#k8_cqc_lang :::"=>"::: )  (Set  "(" "q"  ($#k8_cqc_lang :::"=>"::: )  "p" ")" ) ")" ) "," (Set  "(" "q"  ($#k8_cqc_lang :::"=>"::: )  (Set  "(" "s"  ($#k8_cqc_lang :::"=>"::: )  "p" ")" ) ")" ))) ->   ($#v2_cqc_the1 :::"valid"::: )   ; 
end; 
theorem :: LUKASI_1:44 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A")))  "st" (Bool (Bool (Set (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set  "(" (Set (Var "q"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "r")) ")" )) "is"   ($#v2_cqc_the1 :::"valid"::: )  )) "holds"  (Bool (Set (Set (Var "q"))  ($#k8_cqc_lang :::"=>"::: )  (Set  "(" (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "r")) ")" )) "is"   ($#v2_cqc_the1 :::"valid"::: )  ))) ; 
 
theorem :: LUKASI_1:45 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A")))  "st" (Bool (Bool (Set (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set  "(" (Set (Var "q"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "r")) ")" )) "is"   ($#v2_cqc_the1 :::"valid"::: )  ) & (Bool (Set (Var "q")) "is"   ($#v2_cqc_the1 :::"valid"::: )  )) "holds"  (Bool (Set (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "r"))) "is"   ($#v2_cqc_the1 :::"valid"::: )  ))) ; 
 
theorem :: LUKASI_1:46 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "p")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A"))) "holds"   (Bool  "("  (Bool (Set (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set  "("  ($#k5_cqc_lang :::"VERUM"::: )  (Set (Var "A")) ")" )) "is"   ($#v2_cqc_the1 :::"valid"::: )  ) & (Bool (Set (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set  "("  ($#k5_cqc_lang :::"VERUM"::: )  (Set (Var "A")) ")" ) ")" )  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "p"))) "is"   ($#v2_cqc_the1 :::"valid"::: )  )  ")" ))) ; 
 registrationlet "A" be    ($#m1_qc_lang1 :::"QC-alphabet"::: )  ; let "p", "q" be    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Const "A"))); 
cluster (Set bbbadK2_QC_LANG2("A" "," "p" "," (Set  "(" (Set  "(" "p"  ($#k8_cqc_lang :::"=>"::: )  "q" ")" )  ($#k8_cqc_lang :::"=>"::: )  "q" ")" ))) ->   ($#v2_cqc_the1 :::"valid"::: )   ; 
end; registrationlet "A" be    ($#m1_qc_lang1 :::"QC-alphabet"::: )  ; let "q", "r" be    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Const "A"))); 
cluster (Set bbbadK2_QC_LANG2("A" "," (Set  "(" "q"  ($#k8_cqc_lang :::"=>"::: )  (Set  "(" "q"  ($#k8_cqc_lang :::"=>"::: )  "r" ")" ) ")" ) "," (Set  "(" "q"  ($#k8_cqc_lang :::"=>"::: )  "r" ")" ))) ->   ($#v2_cqc_the1 :::"valid"::: )   ; 
end; 
theorem :: LUKASI_1:47 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "q")) "," (Set (Var "r")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A")))  "st" (Bool (Bool (Set (Set (Var "q"))  ($#k8_cqc_lang :::"=>"::: )  (Set  "(" (Set (Var "q"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "r")) ")" )) "is"   ($#v2_cqc_the1 :::"valid"::: )  )) "holds"  (Bool (Set (Set (Var "q"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "r"))) "is"   ($#v2_cqc_the1 :::"valid"::: )  ))) ; 
 registrationlet "A" be    ($#m1_qc_lang1 :::"QC-alphabet"::: )  ; let "p", "q", "r" be    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Const "A"))); 
cluster (Set bbbadK2_QC_LANG2("A" "," (Set  "(" "p"  ($#k8_cqc_lang :::"=>"::: )  (Set  "(" "q"  ($#k8_cqc_lang :::"=>"::: )  "r" ")" ) ")" ) "," (Set  "(" (Set  "(" "p"  ($#k8_cqc_lang :::"=>"::: )  "q" ")" )  ($#k8_cqc_lang :::"=>"::: )  (Set  "(" "p"  ($#k8_cqc_lang :::"=>"::: )  "r" ")" ) ")" ))) ->   ($#v2_cqc_the1 :::"valid"::: )   ; 
end; 
theorem :: LUKASI_1:48 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A")))  "st" (Bool (Bool (Set (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set  "(" (Set (Var "q"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "r")) ")" )) "is"   ($#v2_cqc_the1 :::"valid"::: )  )) "holds"  (Bool (Set (Set  "(" (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "q")) ")" )  ($#k8_cqc_lang :::"=>"::: )  (Set  "(" (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "r")) ")" )) "is"   ($#v2_cqc_the1 :::"valid"::: )  ))) ; 
 
theorem :: LUKASI_1:49 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A")))  "st" (Bool (Bool (Set (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set  "(" (Set (Var "q"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "r")) ")" )) "is"   ($#v2_cqc_the1 :::"valid"::: )  ) & (Bool (Set (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "q"))) "is"   ($#v2_cqc_the1 :::"valid"::: )  )) "holds"  (Bool (Set (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "r"))) "is"   ($#v2_cqc_the1 :::"valid"::: )  ))) ; 
 registrationlet "A" be    ($#m1_qc_lang1 :::"QC-alphabet"::: )  ; let "p", "q", "r" be    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Const "A"))); 
cluster (Set bbbadK2_QC_LANG2("A" "," (Set  "(" (Set  "(" "p"  ($#k8_cqc_lang :::"=>"::: )  "q" ")" )  ($#k8_cqc_lang :::"=>"::: )  "r" ")" ) "," (Set  "(" "q"  ($#k8_cqc_lang :::"=>"::: )  "r" ")" ))) ->   ($#v2_cqc_the1 :::"valid"::: )   ; 
end; 
theorem :: LUKASI_1:50 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A")))  "st" (Bool (Bool (Set (Set  "(" (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "q")) ")" )  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "r"))) "is"   ($#v2_cqc_the1 :::"valid"::: )  )) "holds"  (Bool (Set (Set (Var "q"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "r"))) "is"   ($#v2_cqc_the1 :::"valid"::: )  ))) ; 
 registrationlet "A" be    ($#m1_qc_lang1 :::"QC-alphabet"::: )  ; let "p", "q", "r" be    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Const "A"))); 
cluster (Set bbbadK2_QC_LANG2("A" "," (Set  "(" "p"  ($#k8_cqc_lang :::"=>"::: )  "q" ")" ) "," (Set  "(" (Set  "(" "r"  ($#k8_cqc_lang :::"=>"::: )  "p" ")" )  ($#k8_cqc_lang :::"=>"::: )  (Set  "(" "r"  ($#k8_cqc_lang :::"=>"::: )  "q" ")" ) ")" ))) ->   ($#v2_cqc_the1 :::"valid"::: )   ; 
end; 
theorem :: LUKASI_1:51 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A")))  "st" (Bool (Bool (Set (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "q"))) "is"   ($#v2_cqc_the1 :::"valid"::: )  )) "holds"  (Bool (Set (Set  "(" (Set (Var "r"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "p")) ")" )  ($#k8_cqc_lang :::"=>"::: )  (Set  "(" (Set (Var "r"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "q")) ")" )) "is"   ($#v2_cqc_the1 :::"valid"::: )  ))) ; 
 registrationlet "A" be    ($#m1_qc_lang1 :::"QC-alphabet"::: )  ; let "p", "q" be    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Const "A"))); 
cluster (Set bbbadK2_QC_LANG2("A" "," (Set  "(" "p"  ($#k8_cqc_lang :::"=>"::: )  "q" ")" ) "," (Set  "(" (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  "q" ")" )  ($#k8_cqc_lang :::"=>"::: )  (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  "p" ")" ) ")" ))) ->   ($#v2_cqc_the1 :::"valid"::: )   ; 
end; registrationlet "A" be    ($#m1_qc_lang1 :::"QC-alphabet"::: )  ; let "p", "q" be    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Const "A"))); 
cluster (Set bbbadK2_QC_LANG2("A" "," (Set  "(" (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  "p" ")" )  ($#k8_cqc_lang :::"=>"::: )  (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  "q" ")" ) ")" ) "," (Set  "(" "q"  ($#k8_cqc_lang :::"=>"::: )  "p" ")" ))) ->   ($#v2_cqc_the1 :::"valid"::: )   ; 
end; 
theorem :: LUKASI_1:52 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A"))) "holds"   (Bool  "("  (Bool (Set (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k8_cqc_lang :::"=>"::: )  (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set (Var "q")) ")" )) "is"   ($#v2_cqc_the1 :::"valid"::: )  ) "iff" (Bool (Set (Set (Var "q"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "p"))) "is"   ($#v2_cqc_the1 :::"valid"::: )  )  ")" ))) ; 
 registrationlet "A" be    ($#m1_qc_lang1 :::"QC-alphabet"::: )  ; let "p" be    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Const "A"))); 
cluster (Set bbbadK2_QC_LANG2("A" "," "p" "," (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  "p" ")" ) ")" ))) ->   ($#v2_cqc_the1 :::"valid"::: )   ; 
end; registrationlet "A" be    ($#m1_qc_lang1 :::"QC-alphabet"::: )  ; let "p" be    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Const "A"))); 
cluster (Set bbbadK2_QC_LANG2("A" "," (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  "p" ")" ) ")" ) "," "p")) ->   ($#v2_cqc_the1 :::"valid"::: )   ; 
end; 
theorem :: LUKASI_1:53 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "p")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A"))) "holds"   (Bool  "("  (Bool (Set   ($#k6_cqc_lang :::"'not'"::: )  (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set (Var "p")) ")" )) "is"   ($#v2_cqc_the1 :::"valid"::: )  ) "iff" (Bool (Set (Var "p")) "is"   ($#v2_cqc_the1 :::"valid"::: )  )  ")" ))) ; 
 registrationlet "A" be    ($#m1_qc_lang1 :::"QC-alphabet"::: )  ; let "p", "q" be    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Const "A"))); 
cluster (Set bbbadK2_QC_LANG2("A" "," (Set  "(" (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  "p" ")" ) ")" )  ($#k8_cqc_lang :::"=>"::: )  "q" ")" ) "," (Set  "(" "p"  ($#k8_cqc_lang :::"=>"::: )  "q" ")" ))) ->   ($#v2_cqc_the1 :::"valid"::: )   ; 
end; 
theorem :: LUKASI_1:54 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A"))) "holds"   (Bool  "("  (Bool (Set (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set (Var "p")) ")" ) ")" )  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "q"))) "is"   ($#v2_cqc_the1 :::"valid"::: )  ) "iff" (Bool (Set (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "q"))) "is"   ($#v2_cqc_the1 :::"valid"::: )  )  ")" ))) ; 
 registrationlet "A" be    ($#m1_qc_lang1 :::"QC-alphabet"::: )  ; let "p", "q" be    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Const "A"))); 
cluster (Set bbbadK2_QC_LANG2("A" "," (Set  "(" "p"  ($#k8_cqc_lang :::"=>"::: )  (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  "q" ")" ) ")" ) ")" ) "," (Set  "(" "p"  ($#k8_cqc_lang :::"=>"::: )  "q" ")" ))) ->   ($#v2_cqc_the1 :::"valid"::: )   ; 
end; 
theorem :: LUKASI_1:55 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A"))) "holds"   (Bool  "("  (Bool (Set (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set (Var "q")) ")" ) ")" )) "is"   ($#v2_cqc_the1 :::"valid"::: )  ) "iff" (Bool (Set (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "q"))) "is"   ($#v2_cqc_the1 :::"valid"::: )  )  ")" ))) ; 
 registrationlet "A" be    ($#m1_qc_lang1 :::"QC-alphabet"::: )  ; let "p", "q" be    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Const "A"))); 
cluster (Set bbbadK2_QC_LANG2("A" "," (Set  "(" "p"  ($#k8_cqc_lang :::"=>"::: )  (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  "q" ")" ) ")" ) "," (Set  "(" "q"  ($#k8_cqc_lang :::"=>"::: )  (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  "p" ")" ) ")" ))) ->   ($#v2_cqc_the1 :::"valid"::: )   ; 
end; 
theorem :: LUKASI_1:56 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A")))  "st" (Bool (Bool (Set (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set (Var "q")) ")" )) "is"   ($#v2_cqc_the1 :::"valid"::: )  )) "holds"  (Bool (Set (Set (Var "q"))  ($#k8_cqc_lang :::"=>"::: )  (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set (Var "p")) ")" )) "is"   ($#v2_cqc_the1 :::"valid"::: )  ))) ; 
 registrationlet "A" be    ($#m1_qc_lang1 :::"QC-alphabet"::: )  ; let "p", "q" be    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Const "A"))); 
cluster (Set bbbadK2_QC_LANG2("A" "," (Set  "(" (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  "p" ")" )  ($#k8_cqc_lang :::"=>"::: )  "q" ")" ) "," (Set  "(" (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  "q" ")" )  ($#k8_cqc_lang :::"=>"::: )  "p" ")" ))) ->   ($#v2_cqc_the1 :::"valid"::: )   ; 
end; 
theorem :: LUKASI_1:57 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A")))  "st" (Bool (Bool (Set (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "q"))) "is"   ($#v2_cqc_the1 :::"valid"::: )  )) "holds"  (Bool (Set (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set (Var "q")) ")" )  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "p"))) "is"   ($#v2_cqc_the1 :::"valid"::: )  ))) ; 
 
theorem :: LUKASI_1:58 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A")))  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A")) ")" )  "st" (Bool (Bool (Set (Var "X"))  ($#r3_cqc_the1 :::"|-"::: )  (Set (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "q"))))) "holds"  (Bool (Set (Var "X"))  ($#r3_cqc_the1 :::"|-"::: )  (Set (Set  "(" (Set (Var "q"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "r")) ")" )  ($#k8_cqc_lang :::"=>"::: )  (Set  "(" (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "r")) ")" )))))) ; 
 
theorem :: LUKASI_1:59 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A")))  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A")) ")" )  "st" (Bool (Bool (Set (Var "X"))  ($#r3_cqc_the1 :::"|-"::: )  (Set (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "q")))) & (Bool (Set (Var "X"))  ($#r3_cqc_the1 :::"|-"::: )  (Set (Set (Var "q"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "r"))))) "holds"  (Bool (Set (Var "X"))  ($#r3_cqc_the1 :::"|-"::: )  (Set (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "r"))))))) ; 
 
theorem :: LUKASI_1:60 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "p")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A")))  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A")) ")" ) "holds"  (Bool (Set (Var "X"))  ($#r3_cqc_the1 :::"|-"::: )  (Set (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "p"))))))) ; 
 
theorem :: LUKASI_1:61 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A")))  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A")) ")" )  "st" (Bool (Bool (Set (Var "X"))  ($#r3_cqc_the1 :::"|-"::: )  (Set (Var "p")))) "holds"  (Bool (Set (Var "X"))  ($#r3_cqc_the1 :::"|-"::: )  (Set (Set (Var "q"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "p"))))))) ; 
 
theorem :: LUKASI_1:62 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A")))  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A")) ")" )  "st" (Bool (Bool (Set (Var "X"))  ($#r3_cqc_the1 :::"|-"::: )  (Set (Var "p")))) "holds"  (Bool (Set (Var "X"))  ($#r3_cqc_the1 :::"|-"::: )  (Set (Set  "(" (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "q")) ")" )  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "q"))))))) ; 
 
theorem :: LUKASI_1:63 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A")))  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A")) ")" )  "st" (Bool (Bool (Set (Var "X"))  ($#r3_cqc_the1 :::"|-"::: )  (Set (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set  "(" (Set (Var "q"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "r")) ")" )))) "holds"  (Bool (Set (Var "X"))  ($#r3_cqc_the1 :::"|-"::: )  (Set (Set (Var "q"))  ($#k8_cqc_lang :::"=>"::: )  (Set  "(" (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "r")) ")" )))))) ; 
 
theorem :: LUKASI_1:64 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A")))  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A")) ")" )  "st" (Bool (Bool (Set (Var "X"))  ($#r3_cqc_the1 :::"|-"::: )  (Set (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set  "(" (Set (Var "q"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "r")) ")" ))) & (Bool (Set (Var "X"))  ($#r3_cqc_the1 :::"|-"::: )  (Set (Var "q")))) "holds"  (Bool (Set (Var "X"))  ($#r3_cqc_the1 :::"|-"::: )  (Set (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "r"))))))) ; 
 
theorem :: LUKASI_1:65 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A")))  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A")) ")" )  "st" (Bool (Bool (Set (Var "X"))  ($#r3_cqc_the1 :::"|-"::: )  (Set (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set  "(" (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "q")) ")" )))) "holds"  (Bool (Set (Var "X"))  ($#r3_cqc_the1 :::"|-"::: )  (Set (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "q"))))))) ; 
 
theorem :: LUKASI_1:66 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A")))  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A")) ")" )  "st" (Bool (Bool (Set (Var "X"))  ($#r3_cqc_the1 :::"|-"::: )  (Set (Set  "(" (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "q")) ")" )  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "r"))))) "holds"  (Bool (Set (Var "X"))  ($#r3_cqc_the1 :::"|-"::: )  (Set (Set (Var "q"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "r"))))))) ; 
 
theorem :: LUKASI_1:67 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A")))  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A")) ")" )  "st" (Bool (Bool (Set (Var "X"))  ($#r3_cqc_the1 :::"|-"::: )  (Set (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set  "(" (Set (Var "q"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "r")) ")" )))) "holds"  (Bool (Set (Var "X"))  ($#r3_cqc_the1 :::"|-"::: )  (Set (Set  "(" (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "q")) ")" )  ($#k8_cqc_lang :::"=>"::: )  (Set  "(" (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "r")) ")" )))))) ; 
 
theorem :: LUKASI_1:68 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A")))  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A")) ")" )  "st" (Bool (Bool (Set (Var "X"))  ($#r3_cqc_the1 :::"|-"::: )  (Set (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set  "(" (Set (Var "q"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "r")) ")" ))) & (Bool (Set (Var "X"))  ($#r3_cqc_the1 :::"|-"::: )  (Set (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "q"))))) "holds"  (Bool (Set (Var "X"))  ($#r3_cqc_the1 :::"|-"::: )  (Set (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "r"))))))) ; 
 
theorem :: LUKASI_1:69 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A")))  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "X"))  ($#r3_cqc_the1 :::"|-"::: )  (Set (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k8_cqc_lang :::"=>"::: )  (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set (Var "q")) ")" ))) "iff" (Bool (Set (Var "X"))  ($#r3_cqc_the1 :::"|-"::: )  (Set (Set (Var "q"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "p"))))  ")" )))) ; 
 
theorem :: LUKASI_1:70 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "p")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A")))  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "X"))  ($#r3_cqc_the1 :::"|-"::: )  (Set   ($#k6_cqc_lang :::"'not'"::: )  (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set (Var "p")) ")" ))) "iff" (Bool (Set (Var "X"))  ($#r3_cqc_the1 :::"|-"::: )  (Set (Var "p")))  ")" )))) ; 
 
theorem :: LUKASI_1:71 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A")))  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "X"))  ($#r3_cqc_the1 :::"|-"::: )  (Set (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set (Var "q")) ")" ) ")" ))) "iff" (Bool (Set (Var "X"))  ($#r3_cqc_the1 :::"|-"::: )  (Set (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "q"))))  ")" )))) ; 
 
theorem :: LUKASI_1:72 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A")))  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "X"))  ($#r3_cqc_the1 :::"|-"::: )  (Set (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set (Var "p")) ")" ) ")" )  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "q")))) "iff" (Bool (Set (Var "X"))  ($#r3_cqc_the1 :::"|-"::: )  (Set (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "q"))))  ")" )))) ; 
 
theorem :: LUKASI_1:73 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A")))  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A")) ")" )  "st" (Bool (Bool (Set (Var "X"))  ($#r3_cqc_the1 :::"|-"::: )  (Set (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set (Var "q")) ")" )))) "holds"  (Bool (Set (Var "X"))  ($#r3_cqc_the1 :::"|-"::: )  (Set (Set (Var "q"))  ($#k8_cqc_lang :::"=>"::: )  (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set (Var "p")) ")" )))))) ; 
 
theorem :: LUKASI_1:74 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A")))  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A")) ")" )  "st" (Bool (Bool (Set (Var "X"))  ($#r3_cqc_the1 :::"|-"::: )  (Set (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "q"))))) "holds"  (Bool (Set (Var "X"))  ($#r3_cqc_the1 :::"|-"::: )  (Set (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set (Var "q")) ")" )  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "p"))))))) ; 
 
theorem :: LUKASI_1:75 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A")))  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A")) ")" )  "st" (Bool (Bool (Set (Var "X"))  ($#r3_cqc_the1 :::"|-"::: )  (Set (Set (Var "p"))  ($#k8_cqc_lang :::"=>"::: )  (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set (Var "q")) ")" ))) & (Bool (Set (Var "X"))  ($#r3_cqc_the1 :::"|-"::: )  (Set (Var "q")))) "holds"  (Bool (Set (Var "X"))  ($#r3_cqc_the1 :::"|-"::: )  (Set   ($#k6_cqc_lang :::"'not'"::: )  (Set (Var "p"))))))) ; 
 
theorem :: LUKASI_1:76 (Bool  "for" (Set (Var "A")) "being"    ($#m1_qc_lang1 :::"QC-alphabet"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A")))  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k3_cqc_lang :::"CQC-WFF"::: )  (Set (Var "A")) ")" )  "st" (Bool (Bool (Set (Var "X"))  ($#r3_cqc_the1 :::"|-"::: )  (Set (Set  "("  ($#k6_cqc_lang :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k8_cqc_lang :::"=>"::: )  (Set (Var "q")))) & (Bool (Set (Var "X"))  ($#r3_cqc_the1 :::"|-"::: )  (Set   ($#k6_cqc_lang :::"'not'"::: )  (Set (Var "q"))))) "holds"  (Bool (Set (Var "X"))  ($#r3_cqc_the1 :::"|-"::: )  (Set (Var "p")))))) ;