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 Th61
.= ((Free p) \/ (Free q)) \/ (Free (q => p)) by Th64
.= ((Free p) \/ (Free q)) \/ ((Free q) \/ (Free p)) by Th64
.= (((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