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