let A be QC-alphabet ; :: thesis: for F, G being Element of QC-WFF A holds Subformulae (F => G) = ((Subformulae F) \/ (Subformulae G)) \/ {('not' G),(F '&' ('not' G)),(F => G)}
let F, G be Element of QC-WFF A; :: thesis: Subformulae (F => G) = ((Subformulae F) \/ (Subformulae G)) \/ {('not' G),(F '&' ('not' G)),(F => G)}
thus Subformulae (F => G) = (Subformulae (F '&' ('not' G))) \/ {(F => G)} by Th88
.= (((Subformulae F) \/ (Subformulae ('not' G))) \/ {(F '&' ('not' G))}) \/ {(F => G)} by Th89
.= (((Subformulae F) \/ ((Subformulae G) \/ {('not' G)})) \/ {(F '&' ('not' G))}) \/ {(F => G)} by Th88
.= ((((Subformulae F) \/ (Subformulae G)) \/ {('not' G)}) \/ {(F '&' ('not' G))}) \/ {(F => G)} by XBOOLE_1:4
.= (((Subformulae F) \/ (Subformulae G)) \/ {('not' G)}) \/ ({(F '&' ('not' G))} \/ {(F => G)}) by XBOOLE_1:4
.= ((Subformulae F) \/ (Subformulae G)) \/ ({('not' G)} \/ ({(F '&' ('not' G))} \/ {(F => G)})) by XBOOLE_1:4
.= ((Subformulae F) \/ (Subformulae G)) \/ ({('not' G)} \/ {(F '&' ('not' G)),(F => G)}) by ENUMSET1:1
.= ((Subformulae F) \/ (Subformulae G)) \/ {('not' G),(F '&' ('not' G)),(F => G)} by ENUMSET1:2 ; :: thesis: verum