let F, G be ZF-formula; Subformulae (F <=> G) = ((Subformulae F) \/ (Subformulae G)) \/ {('not' G),(F '&' ('not' G)),(F => G),('not' F),(G '&' ('not' F)),(G => F),(F <=> G)}
thus Subformulae (F <=> G) =
((Subformulae (F => G)) \/ (Subformulae (G => F))) \/ {(F <=> G)}
by ZF_LANG:83
.=
((((Subformulae F) \/ (Subformulae G)) \/ {('not' G),(F '&' ('not' G)),(F => G)}) \/ (Subformulae (G => F))) \/ {(F <=> G)}
by Th55
.=
((((Subformulae F) \/ (Subformulae G)) \/ {('not' G),(F '&' ('not' G)),(F => G)}) \/ (((Subformulae F) \/ (Subformulae G)) \/ {('not' F),(G '&' ('not' F)),(G => F)})) \/ {(F <=> G)}
by Th55
.=
(((Subformulae F) \/ (Subformulae G)) \/ ((((Subformulae F) \/ (Subformulae G)) \/ {('not' G),(F '&' ('not' G)),(F => G)}) \/ {('not' F),(G '&' ('not' F)),(G => F)})) \/ {(F <=> G)}
by XBOOLE_1:4
.=
(((Subformulae F) \/ (Subformulae G)) \/ (((Subformulae F) \/ (Subformulae G)) \/ ({('not' G),(F '&' ('not' G)),(F => G)} \/ {('not' F),(G '&' ('not' F)),(G => F)}))) \/ {(F <=> G)}
by XBOOLE_1:4
.=
((((Subformulae F) \/ (Subformulae G)) \/ ((Subformulae F) \/ (Subformulae G))) \/ ({('not' G),(F '&' ('not' G)),(F => G)} \/ {('not' F),(G '&' ('not' F)),(G => F)})) \/ {(F <=> G)}
by XBOOLE_1:4
.=
(((Subformulae F) \/ (Subformulae G)) \/ {('not' G),(F '&' ('not' G)),(F => G),('not' F),(G '&' ('not' F)),(G => F)}) \/ {(F <=> G)}
by ENUMSET1:13
.=
((Subformulae F) \/ (Subformulae G)) \/ ({('not' G),(F '&' ('not' G)),(F => G),('not' F),(G '&' ('not' F)),(G => F)} \/ {(F <=> G)})
by XBOOLE_1:4
.=
((Subformulae F) \/ (Subformulae G)) \/ {('not' G),(F '&' ('not' G)),(F => G),('not' F),(G '&' ('not' F)),(G => F),(F <=> G)}
by ENUMSET1:21
; verum