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 = (p => q) '&' (q => p) by QC_LANG2:def 4;
hence Free (p <=> q) = (Free (p => q)) \/ (Free (q => p)) by Th42
.= ((Free p) \/ (Free q)) \/ (Free (q => p)) by Th60
.= ((Free p) \/ (Free q)) \/ ((Free p) \/ (Free q)) by Th60
.= (Free p) \/ (Free q) ;
:: thesis: verum