let p, q be Element of QC-WFF ; :: thesis: Fixed (p => q) = (Fixed p) \/ (Fixed q)
p => q = 'not' (p '&' ('not' q)) by QC_LANG2:def 2;
hence Fixed (p => q) = Fixed (p '&' ('not' q)) by Th50
.= (Fixed p) \/ (Fixed ('not' q)) by Th53
.= (Fixed p) \/ (Fixed q) by Th50 ;
:: thesis: verum