let A be QC-alphabet ; :: thesis: for p, q being Element of CQC-WFF A holds
( p => (p 'or' q) is valid & p => (q 'or' p) is valid )
let p, q be Element of CQC-WFF A; :: thesis: ( p => (p 'or' q) is valid & p => (q 'or' p) is valid )
thus ( p => (p 'or' q) in TAUT A & p => (q 'or' p) in TAUT A ) by PROCAL_1:3, PROCAL_1:4; :: according to CQC_THE1:def 10 :: thesis: verum