let F, G be ZF-formula; :: thesis: Subformulae (F 'or' G) = ((Subformulae F) \/ (Subformulae G)) \/ {('not' G),('not' F),(('not' F) '&' ('not' G)),(F 'or' G)}
thus Subformulae (F 'or' G) = (Subformulae (('not' F) '&' ('not' G))) \/ {(F 'or' G)} by ZF_LANG:82
.= (((Subformulae ('not' F)) \/ (Subformulae ('not' G))) \/ {(('not' F) '&' ('not' G))}) \/ {(F 'or' G)} by ZF_LANG:83
.= (((Subformulae ('not' F)) \/ ((Subformulae G) \/ {('not' G)})) \/ {(('not' F) '&' ('not' G))}) \/ {(F 'or' G)} by ZF_LANG:82
.= ((((Subformulae F) \/ {('not' F)}) \/ ((Subformulae G) \/ {('not' G)})) \/ {(('not' F) '&' ('not' G))}) \/ {(F 'or' G)} by ZF_LANG:82
.= (((Subformulae F) \/ (((Subformulae G) \/ {('not' G)}) \/ {('not' F)})) \/ {(('not' F) '&' ('not' G))}) \/ {(F 'or' G)} by XBOOLE_1:4
.= (((Subformulae F) \/ ((Subformulae G) \/ ({('not' G)} \/ {('not' F)}))) \/ {(('not' F) '&' ('not' G))}) \/ {(F 'or' G)} by XBOOLE_1:4
.= (((Subformulae F) \/ ((Subformulae G) \/ {('not' G),('not' F)})) \/ {(('not' F) '&' ('not' G))}) \/ {(F 'or' G)} by ENUMSET1:1
.= ((((Subformulae F) \/ (Subformulae G)) \/ {('not' G),('not' F)}) \/ {(('not' F) '&' ('not' G))}) \/ {(F 'or' G)} by XBOOLE_1:4
.= (((Subformulae F) \/ (Subformulae G)) \/ {('not' G),('not' F)}) \/ ({(('not' F) '&' ('not' G))} \/ {(F 'or' G)}) by XBOOLE_1:4
.= (((Subformulae F) \/ (Subformulae G)) \/ {('not' G),('not' F)}) \/ {(('not' F) '&' ('not' G)),(F 'or' G)} by ENUMSET1:1
.= ((Subformulae F) \/ (Subformulae G)) \/ ({('not' G),('not' F)} \/ {(('not' F) '&' ('not' G)),(F 'or' G)}) by XBOOLE_1:4
.= ((Subformulae F) \/ (Subformulae G)) \/ {('not' G),('not' F),(('not' F) '&' ('not' G)),(F 'or' G)} by ENUMSET1:5 ; :: thesis: verum