:: LUKASI_1 semantic presentation

begin

theorem :: LUKASI_1:1
for A being ( ( ) ( ) QC-alphabet )
for p, q, r being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) holds (p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => ((q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => r : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => (p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => r : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) in TAUT A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of K6((CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) ;

theorem :: LUKASI_1:2
for A being ( ( ) ( ) QC-alphabet )
for p, q, r being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) st p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) in TAUT A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of K6((CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) holds
(q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => r : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => (p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => r : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) in TAUT A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of K6((CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) ;

theorem :: LUKASI_1:3
for A being ( ( ) ( ) QC-alphabet )
for p, q, r being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) st p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) in TAUT A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of K6((CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) & q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => r : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) in TAUT A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of K6((CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) holds
p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => r : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) in TAUT A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of K6((CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) ;

theorem :: LUKASI_1:4
for A being ( ( ) ( ) QC-alphabet )
for p being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) holds p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) in TAUT A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of K6((CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) ;

theorem :: LUKASI_1:5
for A being ( ( ) ( ) QC-alphabet )
for q, p being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) holds q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => (p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) in TAUT A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of K6((CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) ;

theorem :: LUKASI_1:6
for A being ( ( ) ( ) QC-alphabet )
for p, q, r being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) holds ((p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => r : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => (q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => r : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) in TAUT A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of K6((CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) ;

theorem :: LUKASI_1:7
for A being ( ( ) ( ) QC-alphabet )
for q, p being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) holds q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => ((q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) in TAUT A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of K6((CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) ;

theorem :: LUKASI_1:8
for A being ( ( ) ( ) QC-alphabet )
for s, q, p being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) holds (s : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => (q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => (q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => (s : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) in TAUT A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of K6((CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) ;

theorem :: LUKASI_1:9
for A being ( ( ) ( ) QC-alphabet )
for q, r, p being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) holds (q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => r : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => ((p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => (p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => r : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) in TAUT A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of K6((CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) ;

theorem :: LUKASI_1:10
for A being ( ( ) ( ) QC-alphabet )
for q, r being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) holds (q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => (q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => r : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => (q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => r : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) in TAUT A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of K6((CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) ;

theorem :: LUKASI_1:11
for A being ( ( ) ( ) QC-alphabet )
for p, q, r being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) holds (p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => (q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => r : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => ((p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => (p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => r : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) in TAUT A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of K6((CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) ;

theorem :: LUKASI_1:12
for A being ( ( ) ( ) QC-alphabet )
for p being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) holds ('not' (VERUM A : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) in TAUT A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of K6((CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) ;

theorem :: LUKASI_1:13
for A being ( ( ) ( ) QC-alphabet )
for q, p being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) st q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) in TAUT A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of K6((CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) holds
p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) in TAUT A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of K6((CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) ;

theorem :: LUKASI_1:14
for A being ( ( ) ( ) QC-alphabet )
for p, q being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) st p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) in TAUT A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of K6((CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) holds
(p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) in TAUT A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of K6((CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) ;

theorem :: LUKASI_1:15
for A being ( ( ) ( ) QC-alphabet )
for s, q, p being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) st s : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => (q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) in TAUT A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of K6((CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) holds
q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => (s : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) in TAUT A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of K6((CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) ;

theorem :: LUKASI_1:16
for A being ( ( ) ( ) QC-alphabet )
for s, q, p being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) st s : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => (q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) in TAUT A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of K6((CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) & q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) in TAUT A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of K6((CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) holds
s : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) in TAUT A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of K6((CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) ;

theorem :: LUKASI_1:17
for A being ( ( ) ( ) QC-alphabet )
for s, q, p being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) st s : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => (q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) in TAUT A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of K6((CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) & q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) in TAUT A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of K6((CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) & s : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) in TAUT A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of K6((CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) holds
p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) in TAUT A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of K6((CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) ;

theorem :: LUKASI_1:18
for A being ( ( ) ( ) QC-alphabet )
for q, r being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) st q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => (q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => r : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) in TAUT A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of K6((CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) holds
q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => r : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) in TAUT A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of K6((CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) ;

theorem :: LUKASI_1:19
for A being ( ( ) ( ) QC-alphabet )
for p, q, r being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) st p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => (q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => r : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) in TAUT A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of K6((CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) holds
(p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => (p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => r : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) in TAUT A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of K6((CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) ;

theorem :: LUKASI_1:20
for A being ( ( ) ( ) QC-alphabet )
for p, q, r being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) st p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => (q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => r : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) in TAUT A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of K6((CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) & p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) in TAUT A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of K6((CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) holds
p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => r : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) in TAUT A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of K6((CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) ;

theorem :: LUKASI_1:21
for A being ( ( ) ( ) QC-alphabet )
for p, q, r being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) st p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => (q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => r : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) in TAUT A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of K6((CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) & p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) in TAUT A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of K6((CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) & p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) in TAUT A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of K6((CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) holds
r : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) in TAUT A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of K6((CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) ;

theorem :: LUKASI_1:22
for A being ( ( ) ( ) QC-alphabet )
for p, q, r, s being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) st p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => (q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => r : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) in TAUT A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of K6((CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) & p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => (r : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => s : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) in TAUT A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of K6((CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) holds
p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => (q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => s : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) in TAUT A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of K6((CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) ;

theorem :: LUKASI_1:23
for A being ( ( ) ( ) QC-alphabet )
for p being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) holds p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => (VERUM A : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) in TAUT A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of K6((CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) ;

theorem :: LUKASI_1:24
for A being ( ( ) ( ) QC-alphabet )
for p, q being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) holds (('not' p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => ('not' q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => (q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) in TAUT A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of K6((CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) ;

theorem :: LUKASI_1:25
for A being ( ( ) ( ) QC-alphabet )
for p being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) holds ('not' ('not' p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) in TAUT A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of K6((CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) ;

theorem :: LUKASI_1:26
for A being ( ( ) ( ) QC-alphabet )
for p, q being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) holds (p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => (('not' q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => ('not' p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) in TAUT A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of K6((CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) ;

theorem :: LUKASI_1:27
for A being ( ( ) ( ) QC-alphabet )
for p being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) holds p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => ('not' ('not' p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) in TAUT A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of K6((CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) ;

theorem :: LUKASI_1:28
for A being ( ( ) ( ) QC-alphabet )
for p, q being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) holds
( (('not' ('not' p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => (p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) in TAUT A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of K6((CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) & (p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => (('not' ('not' p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) in TAUT A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of K6((CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: LUKASI_1:29
for A being ( ( ) ( ) QC-alphabet )
for p, q being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) holds
( (p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => ('not' ('not' q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => (p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) in TAUT A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of K6((CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) & (p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => (p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => ('not' ('not' q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) in TAUT A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of K6((CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: LUKASI_1:30
for A being ( ( ) ( ) QC-alphabet )
for p, q being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) holds (p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => ('not' q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => (q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => ('not' p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) in TAUT A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of K6((CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) ;

theorem :: LUKASI_1:31
for A being ( ( ) ( ) QC-alphabet )
for p, q being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) holds (('not' p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => (('not' q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) in TAUT A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of K6((CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) ;

theorem :: LUKASI_1:32
for A being ( ( ) ( ) QC-alphabet )
for p being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) holds (p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => ('not' p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => ('not' p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) in TAUT A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of K6((CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) ;

theorem :: LUKASI_1:33
for A being ( ( ) ( ) QC-alphabet )
for p, q being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) holds ('not' p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => (p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) in TAUT A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of K6((CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) ;

theorem :: LUKASI_1:34
for A being ( ( ) ( ) QC-alphabet )
for p, q being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) holds
( p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) in TAUT A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of K6((CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) iff ('not' q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => ('not' p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) in TAUT A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of K6((CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: LUKASI_1:35
for A being ( ( ) ( ) QC-alphabet )
for p, q being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) st ('not' p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => ('not' q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) in TAUT A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of K6((CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) holds
q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) in TAUT A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of K6((CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) ;

theorem :: LUKASI_1:36
for A being ( ( ) ( ) QC-alphabet )
for p being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) holds
( p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) in TAUT A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of K6((CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) iff 'not' ('not' p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) in TAUT A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of K6((CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: LUKASI_1:37
for A being ( ( ) ( ) QC-alphabet )
for p, q being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) holds
( p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) in TAUT A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of K6((CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) iff p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => ('not' ('not' q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) in TAUT A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of K6((CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: LUKASI_1:38
for A being ( ( ) ( ) QC-alphabet )
for p, q being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) holds
( p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) in TAUT A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of K6((CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) iff ('not' ('not' p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) in TAUT A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of K6((CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: LUKASI_1:39
for A being ( ( ) ( ) QC-alphabet )
for p, q being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) st p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => ('not' q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) in TAUT A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of K6((CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) holds
q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => ('not' p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) in TAUT A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of K6((CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) ;

theorem :: LUKASI_1:40
for A being ( ( ) ( ) QC-alphabet )
for p, q being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) st ('not' p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) in TAUT A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of K6((CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) holds
('not' q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) in TAUT A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of K6((CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) ;

registration
let A be ( ( ) ( ) QC-alphabet ) ;
let p, q, r be ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ;
cluster K170(A : ( ( ) ( ) QC-alphabet ) ,(p : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => q : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ,((q : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => r : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => (p : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => r : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of QC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( V1() ) ( V1() ) set ) ) -> valid ;
end;

theorem :: LUKASI_1:41
for A being ( ( ) ( ) QC-alphabet )
for p, q, r being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) st p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) is valid holds
(q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => r : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => (p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => r : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) is valid ;

theorem :: LUKASI_1:42
for A being ( ( ) ( ) QC-alphabet )
for p, q, r being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) st p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) is valid & q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => r : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) is valid holds
p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => r : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) is valid ;

registration
let A be ( ( ) ( ) QC-alphabet ) ;
let p be ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ;
cluster K170(A : ( ( ) ( ) QC-alphabet ) ,p : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ,p : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of QC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( V1() ) ( V1() ) set ) ) -> valid ;
end;

registration
let A be ( ( ) ( ) QC-alphabet ) ;
let p, q be ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ;
cluster K170(A : ( ( ) ( ) QC-alphabet ) ,p : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ,(q : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => p : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of QC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( V1() ) ( V1() ) set ) ) -> valid ;
end;

theorem :: LUKASI_1:43
for A being ( ( ) ( ) QC-alphabet )
for p, q being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) st p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) is valid holds
q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) is valid ;

registration
let A be ( ( ) ( ) QC-alphabet ) ;
let p, q, s be ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ;
cluster K170(A : ( ( ) ( ) QC-alphabet ) ,(s : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => (q : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => p : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ,(q : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => (s : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => p : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of QC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( V1() ) ( V1() ) set ) ) -> valid ;
end;

theorem :: LUKASI_1:44
for A being ( ( ) ( ) QC-alphabet )
for p, q, r being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) st p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => (q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => r : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) is valid holds
q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => (p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => r : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) is valid ;

theorem :: LUKASI_1:45
for A being ( ( ) ( ) QC-alphabet )
for p, q, r being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) st p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => (q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => r : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) is valid & q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) is valid holds
p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => r : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) is valid ;

theorem :: LUKASI_1:46
for A being ( ( ) ( ) QC-alphabet )
for p being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) holds
( p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => (VERUM A : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) is valid & ('not' (VERUM A : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) is valid ) ;

registration
let A be ( ( ) ( ) QC-alphabet ) ;
let p, q be ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ;
cluster K170(A : ( ( ) ( ) QC-alphabet ) ,p : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ,((p : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => q : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => q : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of QC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( V1() ) ( V1() ) set ) ) -> valid ;
end;

registration
let A be ( ( ) ( ) QC-alphabet ) ;
let q, r be ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ;
cluster K170(A : ( ( ) ( ) QC-alphabet ) ,(q : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => (q : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => r : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ,(q : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => r : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of QC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( V1() ) ( V1() ) set ) ) -> valid ;
end;

theorem :: LUKASI_1:47
for A being ( ( ) ( ) QC-alphabet )
for q, r being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) st q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => (q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => r : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) is valid holds
q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => r : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) is valid ;

registration
let A be ( ( ) ( ) QC-alphabet ) ;
let p, q, r be ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ;
cluster K170(A : ( ( ) ( ) QC-alphabet ) ,(p : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => (q : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => r : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ,((p : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => q : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => (p : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => r : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of QC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( V1() ) ( V1() ) set ) ) -> valid ;
end;

theorem :: LUKASI_1:48
for A being ( ( ) ( ) QC-alphabet )
for p, q, r being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) st p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => (q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => r : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) is valid holds
(p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => (p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => r : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) is valid ;

theorem :: LUKASI_1:49
for A being ( ( ) ( ) QC-alphabet )
for p, q, r being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) st p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => (q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => r : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) is valid & p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) is valid holds
p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => r : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) is valid ;

registration
let A be ( ( ) ( ) QC-alphabet ) ;
let p, q, r be ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ;
cluster K170(A : ( ( ) ( ) QC-alphabet ) ,((p : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => q : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => r : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ,(q : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => r : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of QC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( V1() ) ( V1() ) set ) ) -> valid ;
end;

theorem :: LUKASI_1:50
for A being ( ( ) ( ) QC-alphabet )
for p, q, r being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) st (p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => r : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) is valid holds
q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => r : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) is valid ;

registration
let A be ( ( ) ( ) QC-alphabet ) ;
let p, q, r be ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ;
cluster K170(A : ( ( ) ( ) QC-alphabet ) ,(p : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => q : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ,((r : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => p : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => (r : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => q : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of QC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( V1() ) ( V1() ) set ) ) -> valid ;
end;

theorem :: LUKASI_1:51
for A being ( ( ) ( ) QC-alphabet )
for p, q, r being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) st p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) is valid holds
(r : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => (r : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) is valid ;

registration
let A be ( ( ) ( ) QC-alphabet ) ;
let p, q be ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ;
cluster K170(A : ( ( ) ( ) QC-alphabet ) ,(p : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => q : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ,(('not' q : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => ('not' p : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of QC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( V1() ) ( V1() ) set ) ) -> valid ;
end;

registration
let A be ( ( ) ( ) QC-alphabet ) ;
let p, q be ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ;
cluster K170(A : ( ( ) ( ) QC-alphabet ) ,(('not' p : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => ('not' q : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ,(q : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => p : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of QC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( V1() ) ( V1() ) set ) ) -> valid ;
end;

theorem :: LUKASI_1:52
for A being ( ( ) ( ) QC-alphabet )
for p, q being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) holds
( ('not' p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => ('not' q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) is valid iff q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) is valid ) ;

registration
let A be ( ( ) ( ) QC-alphabet ) ;
let p be ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ;
cluster K170(A : ( ( ) ( ) QC-alphabet ) ,p : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ,('not' ('not' p : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of QC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( V1() ) ( V1() ) set ) ) -> valid ;
end;

registration
let A be ( ( ) ( ) QC-alphabet ) ;
let p be ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ;
cluster K170(A : ( ( ) ( ) QC-alphabet ) ,('not' ('not' p : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ,p : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of QC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( V1() ) ( V1() ) set ) ) -> valid ;
end;

theorem :: LUKASI_1:53
for A being ( ( ) ( ) QC-alphabet )
for p being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) holds
( 'not' ('not' p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) is valid iff p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) is valid ) ;

registration
let A be ( ( ) ( ) QC-alphabet ) ;
let p, q be ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ;
cluster K170(A : ( ( ) ( ) QC-alphabet ) ,(('not' ('not' p : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => q : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ,(p : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => q : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of QC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( V1() ) ( V1() ) set ) ) -> valid ;
end;

theorem :: LUKASI_1:54
for A being ( ( ) ( ) QC-alphabet )
for p, q being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) holds
( ('not' ('not' p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) is valid iff p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) is valid ) ;

registration
let A be ( ( ) ( ) QC-alphabet ) ;
let p, q be ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ;
cluster K170(A : ( ( ) ( ) QC-alphabet ) ,(p : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => ('not' ('not' q : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ,(p : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => q : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of QC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( V1() ) ( V1() ) set ) ) -> valid ;
end;

theorem :: LUKASI_1:55
for A being ( ( ) ( ) QC-alphabet )
for p, q being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) holds
( p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => ('not' ('not' q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) is valid iff p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) is valid ) ;

registration
let A be ( ( ) ( ) QC-alphabet ) ;
let p, q be ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ;
cluster K170(A : ( ( ) ( ) QC-alphabet ) ,(p : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => ('not' q : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ,(q : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => ('not' p : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of QC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( V1() ) ( V1() ) set ) ) -> valid ;
end;

theorem :: LUKASI_1:56
for A being ( ( ) ( ) QC-alphabet )
for p, q being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) st p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => ('not' q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) is valid holds
q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => ('not' p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) is valid ;

registration
let A be ( ( ) ( ) QC-alphabet ) ;
let p, q be ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ;
cluster K170(A : ( ( ) ( ) QC-alphabet ) ,(('not' p : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => q : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ,(('not' q : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => p : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF A : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of QC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( V1() ) ( V1() ) set ) ) -> valid ;
end;

theorem :: LUKASI_1:57
for A being ( ( ) ( ) QC-alphabet )
for p, q being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) st ('not' p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) is valid holds
('not' q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) is valid ;

theorem :: LUKASI_1:58
for A being ( ( ) ( ) QC-alphabet )
for p, q, r being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) )
for X being ( ( ) ( ) Subset of ( ( ) ( ) set ) ) st X : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) |- p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) holds
X : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) |- (q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => r : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => (p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => r : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: LUKASI_1:59
for A being ( ( ) ( ) QC-alphabet )
for p, q, r being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) )
for X being ( ( ) ( ) Subset of ( ( ) ( ) set ) ) st X : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) |- p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) & X : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) |- q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => r : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) holds
X : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) |- p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => r : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: LUKASI_1:60
for A being ( ( ) ( ) QC-alphabet )
for p being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) )
for X being ( ( ) ( ) Subset of ( ( ) ( ) set ) ) holds X : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) |- p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( valid ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: LUKASI_1:61
for A being ( ( ) ( ) QC-alphabet )
for p, q being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) )
for X being ( ( ) ( ) Subset of ( ( ) ( ) set ) ) st X : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) |- p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) holds
X : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) |- q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: LUKASI_1:62
for A being ( ( ) ( ) QC-alphabet )
for p, q being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) )
for X being ( ( ) ( ) Subset of ( ( ) ( ) set ) ) st X : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) |- p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) holds
X : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) |- (p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: LUKASI_1:63
for A being ( ( ) ( ) QC-alphabet )
for p, q, r being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) )
for X being ( ( ) ( ) Subset of ( ( ) ( ) set ) ) st X : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) |- p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => (q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => r : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) holds
X : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) |- q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => (p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => r : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: LUKASI_1:64
for A being ( ( ) ( ) QC-alphabet )
for p, q, r being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) )
for X being ( ( ) ( ) Subset of ( ( ) ( ) set ) ) st X : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) |- p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => (q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => r : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) & X : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) |- q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) holds
X : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) |- p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => r : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: LUKASI_1:65
for A being ( ( ) ( ) QC-alphabet )
for p, q being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) )
for X being ( ( ) ( ) Subset of ( ( ) ( ) set ) ) st X : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) |- p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => (p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) holds
X : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) |- p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: LUKASI_1:66
for A being ( ( ) ( ) QC-alphabet )
for p, q, r being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) )
for X being ( ( ) ( ) Subset of ( ( ) ( ) set ) ) st X : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) |- (p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => r : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) holds
X : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) |- q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => r : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: LUKASI_1:67
for A being ( ( ) ( ) QC-alphabet )
for p, q, r being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) )
for X being ( ( ) ( ) Subset of ( ( ) ( ) set ) ) st X : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) |- p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => (q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => r : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) holds
X : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) |- (p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => (p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => r : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: LUKASI_1:68
for A being ( ( ) ( ) QC-alphabet )
for p, q, r being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) )
for X being ( ( ) ( ) Subset of ( ( ) ( ) set ) ) st X : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) |- p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => (q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => r : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) & X : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) |- p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) holds
X : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) |- p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => r : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: LUKASI_1:69
for A being ( ( ) ( ) QC-alphabet )
for p, q being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) )
for X being ( ( ) ( ) Subset of ( ( ) ( ) set ) ) holds
( X : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) |- ('not' p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => ('not' q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) iff X : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) |- q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) ;

theorem :: LUKASI_1:70
for A being ( ( ) ( ) QC-alphabet )
for p being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) )
for X being ( ( ) ( ) Subset of ( ( ) ( ) set ) ) holds
( X : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) |- 'not' ('not' p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) iff X : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) |- p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) ;

theorem :: LUKASI_1:71
for A being ( ( ) ( ) QC-alphabet )
for p, q being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) )
for X being ( ( ) ( ) Subset of ( ( ) ( ) set ) ) holds
( X : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) |- p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => ('not' ('not' q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) iff X : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) |- p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) ;

theorem :: LUKASI_1:72
for A being ( ( ) ( ) QC-alphabet )
for p, q being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) )
for X being ( ( ) ( ) Subset of ( ( ) ( ) set ) ) holds
( X : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) |- ('not' ('not' p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) iff X : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) |- p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) ;

theorem :: LUKASI_1:73
for A being ( ( ) ( ) QC-alphabet )
for p, q being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) )
for X being ( ( ) ( ) Subset of ( ( ) ( ) set ) ) st X : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) |- p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => ('not' q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) holds
X : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) |- q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => ('not' p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: LUKASI_1:74
for A being ( ( ) ( ) QC-alphabet )
for p, q being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) )
for X being ( ( ) ( ) Subset of ( ( ) ( ) set ) ) st X : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) |- ('not' p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) holds
X : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) |- ('not' q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: LUKASI_1:75
for A being ( ( ) ( ) QC-alphabet )
for p, q being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) )
for X being ( ( ) ( ) Subset of ( ( ) ( ) set ) ) st X : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) |- p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => ('not' q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) & X : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) |- q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) holds
X : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) |- 'not' p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: LUKASI_1:76
for A being ( ( ) ( ) QC-alphabet )
for p, q being ( ( ) ( ) Element of CQC-WFF A : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) )
for X being ( ( ) ( ) Subset of ( ( ) ( ) set ) ) st X : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) |- ('not' p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) => q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) & X : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) |- 'not' q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) holds
X : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) |- p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( V1() ) Element of K6((QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( V1() ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ;