let p, q be Element of QC-WFF ; :: thesis: Free (p 'or' q) = (Free p) \/ (Free q)
p 'or' q = 'not' (('not' p) '&' ('not' q)) by QC_LANG2:def 3;
hence Free (p 'or' q) = Free (('not' p) '&' ('not' q)) by Th50
.= (Free ('not' p)) \/ (Free ('not' q)) by Th53
.= (Free p) \/ (Free ('not' q)) by Th50
.= (Free p) \/ (Free q) by Th50 ;
:: thesis: verum