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