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 Th163
.= (-- (r -- F)) /\ (-- (r -- G)) by Th12
.= (-- (r -- F)) /\ (G -- r) by Th66
.= (F -- r) /\ (G -- r) by Th66 ; :: thesis: verum