let p, q, p1, q1 be Element of QC-WFF ; :: 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:46;
then ( 'not' p = 'not' p1 & 'not' q = 'not' q1 ) by Th3;
hence ( p = p1 & q = q1 ) by FINSEQ_1:46; :: thesis: verum