let Al be QC-alphabet ; for p, q 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) holds
( ( J,v |= p or J,v |= q ) iff J,v |= p 'or' q )
let p, q 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) holds
( ( J,v |= p or J,v |= q ) iff J,v |= p 'or' q )
let A be non empty set ; for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A) holds
( ( J,v |= p or J,v |= q ) iff J,v |= p 'or' q )
let J be interpretation of Al,A; for v being Element of Valuations_in (Al,A) holds
( ( J,v |= p or J,v |= q ) iff J,v |= p 'or' q )
let v be Element of Valuations_in (Al,A); ( ( J,v |= p or J,v |= q ) iff J,v |= p 'or' q )
thus
( ( J,v |= p or J,v |= q ) implies J,v |= p 'or' q )
( not J,v |= p 'or' q or J,v |= p or J,v |= q )
thus
( not J,v |= p 'or' q or J,v |= p or J,v |= q )
verum