let F, G be ext-real-membered set ; :: thesis: for r being Real holds r -- (F \ G) = (r -- F) \ (r -- G)
let r be Real; :: thesis: r -- (F \ G) = (r -- F) \ (r -- G)
thus r -- (F \ G) = r ++ ((-- F) \ (-- G)) by Th7
.= (r ++ (-- F)) \ (r ++ (-- G)) by Th139
.= (r -- F) \ (r -- G) ; :: thesis: verum