let p, q be ZF-formula; :: thesis: Free (p 'or' q) = (Free p) \/ (Free q)
thus Free (p 'or' q) = Free (('not' p) '&' ('not' q)) by Th60
.= (Free ('not' p)) \/ (Free ('not' q)) by Th61
.= (Free p) \/ (Free ('not' q)) by Th60
.= (Free p) \/ (Free q) by Th60 ; :: thesis: verum