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