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