let X be Subset of CQC-WFF; :: thesis: for p being Element of CQC-WFF
for A being non empty set
for J being interpretation of A
for v being Element of Valuations_in A st X |= p holds
not J,v |= X \/ {('not' p)}
let p be Element of CQC-WFF ; :: thesis: for A being non empty set
for J being interpretation of A
for v being Element of Valuations_in A st X |= p holds
not J,v |= X \/ {('not' p)}
let A be non empty set ; :: thesis: for J being interpretation of A
for v being Element of Valuations_in A st X |= p holds
not J,v |= X \/ {('not' p)}
let J be interpretation of A; :: thesis: for v being Element of Valuations_in A st X |= p holds
not J,v |= X \/ {('not' p)}
let v be Element of Valuations_in 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