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),('not' F),(G '&' ('not' F)),(G => F),(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),('not' F),(G '&' ('not' F)),(G => F),(F <=> G)}
thus Subformulae (F <=> G) = ((Subformulae (F => G)) \/ (Subformulae (G => F))) \/ {(F <=> G)} by Th89
.= ((((Subformulae F) \/ (Subformulae G)) \/ {('not' G),(F '&' ('not' G)),(F => G)}) \/ (Subformulae (G => F))) \/ {(F <=> G)} by Th91
.= ((((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 Th91
.= (((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 ; :: thesis: verum