let F, G be ZF-formula; :: 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 ZF_LANG:82
.= (((Subformulae F) \/ (Subformulae ('not' G))) \/ {(F '&' ('not' G))}) \/ {(F => G)} by ZF_LANG:83
.= (((Subformulae F) \/ ((Subformulae G) \/ {('not' G)})) \/ {(F '&' ('not' G))}) \/ {(F => G)} by ZF_LANG:82
.= ((((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