let p, q be ZF-formula; :: thesis: Free (p <=> q) = (Free p) \/ (Free q)
thus Free (p <=> q) = (Free (p => q)) \/ (Free (q => p)) by Th66
.= ((Free p) \/ (Free q)) \/ (Free (q => p)) by Th69
.= ((Free p) \/ (Free q)) \/ ((Free q) \/ (Free p)) by Th69
.= (((Free p) \/ (Free q)) \/ (Free q)) \/ (Free p) by XBOOLE_1:4
.= ((Free p) \/ ((Free q) \/ (Free q))) \/ (Free p) by XBOOLE_1:4
.= ((Free p) \/ (Free p)) \/ (Free q) by XBOOLE_1:4
.= (Free p) \/ (Free q) ; :: thesis: verum