let Al be QC-alphabet ; :: thesis: 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); :: thesis: 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; :: thesis: 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 ; :: thesis: 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; :: thesis: 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); :: thesis: ( X |= p implies not J,v |= X \/ {('not' p)} )
assume A1: X |= p ; :: thesis: not J,v |= X \/ {('not' p)}
assume A2: J,v |= X \/ {('not' p)} ; :: thesis: 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; :: thesis: verum