let F, G be ext-real-membered set ; :: thesis: -- (F -- G) = (-- F) ++ G
thus -- (F -- G) = (-- F) -- (-- G) by Lm4
.= (-- F) ++ G ; :: thesis: verum