let Al be QC-alphabet ; for X being Subset of (CQC-WFF Al)
for p being Element of CQC-WFF Al
for A being non empty set
for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A) st X |= p holds
not J,v |= X \/ {('not' p)}
let X be Subset of (CQC-WFF Al); for p being Element of CQC-WFF Al
for A being non empty set
for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A) st X |= p holds
not J,v |= X \/ {('not' p)}
let p be Element of CQC-WFF Al; for A being non empty set
for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A) st X |= p holds
not J,v |= X \/ {('not' p)}
let A be non empty set ; for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A) st X |= p holds
not J,v |= X \/ {('not' p)}
let J be interpretation of Al,A; for v being Element of Valuations_in (Al,A) st X |= p holds
not J,v |= X \/ {('not' p)}
let v be Element of Valuations_in (Al,A); ( X |= p implies not J,v |= X \/ {('not' p)} )
assume A1:
X |= p
; not J,v |= X \/ {('not' p)}
assume A2:
J,v |= X \/ {('not' p)}
; contradiction
then A3:
J,v |= X
by Th35, XBOOLE_1:7;
A4:
{('not' p)} c= X \/ {('not' p)}
by XBOOLE_1:7;
'not' p in {('not' p)}
by TARSKI:def 1;
then
J,v |= 'not' p
by A2, A4, CALCUL_1:def 11;
then
not J,v |= p
by VALUAT_1:17;
hence
contradiction
by A1, A3, CALCUL_1:def 12; verum