let A be QC-alphabet ; :: thesis: for p, q being Element of QC-WFF A holds Free (p => q) = (Free p) \/ (Free q)
let p, q be Element of QC-WFF A; :: thesis: Free (p => q) = (Free p) \/ (Free q)
p => q = 'not' (p '&' ('not' q)) by QC_LANG2:def 2;
hence Free (p => q) = Free (p '&' ('not' q)) by Th39
.= (Free p) \/ (Free ('not' q)) by Th42
.= (Free p) \/ (Free q) by Th39 ;
:: thesis: verum