let Al be QC-alphabet ; :: thesis: 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; :: thesis: 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 ; :: thesis: 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; :: thesis: 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); :: thesis: ( ( 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 ) :: thesis: ( not J,v |= p 'or' q or J,v |= p or J,v |= q )

proof

assume ( J,v |= p or J,v |= q ) ; :: thesis: J,v |= p 'or' q
then ( not J,v |= 'not' p or not J,v |= 'not' q ) by VALUAT_1:17;
then not J,v |= ('not' p) '&' ('not' q) by VALUAT_1:18;
then J,v |= 'not' (('not' p) '&' ('not' q)) by VALUAT_1:17;
hence J,v |= p 'or' q by QC_LANG2:def 3; :: thesis: verum

end;

thus ( not J,v |= p 'or' q or J,v |= p or J,v |= q ) :: thesis: verum

proof

assume J,v |= p 'or' q ; :: thesis: ( J,v |= p or J,v |= q )
then J,v |= 'not' (('not' p) '&' ('not' q)) by QC_LANG2:def 3;
then ( not J,v |= 'not' p or not J,v |= 'not' q ) by VALUAT_1:17, VALUAT_1:18;
hence ( J,v |= p or J,v |= q ) by VALUAT_1:17; :: thesis: verum

end;