let A be QC-alphabet ; :: thesis: for p, q, p1, q1 being Element of QC-WFF A st p 'or' q = p1 'or' q1 holds
( p = p1 & q = q1 )
let p, q, p1, q1 be Element of QC-WFF A; :: thesis: ( p 'or' q = p1 'or' q1 implies ( p = p1 & q = q1 ) )
assume p 'or' q = p1 'or' q1 ; :: thesis: ( p = p1 & q = q1 )
then ('not' p) '&' ('not' q) = ('not' p1) '&' ('not' q1) by FINSEQ_1:33;
then ( 'not' p = 'not' p1 & 'not' q = 'not' q1 ) by Th2;
hence ( p = p1 & q = q1 ) by FINSEQ_1:33; :: thesis: verum