let p, q be Element of QC-WFF ; :: 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 Th53
.= ((Free p) \/ (Free q)) \/ (Free (q => p)) by Th72
.= ((Free p) \/ (Free q)) \/ ((Free p) \/ (Free q)) by Th72
.= (Free p) \/ (Free q) ;
:: thesis: verum