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 Th157
.= (-- (r -- F)) /\ (-- (r -- G)) by Th6
.= (-- (r -- F)) /\ (G -- r) by Th60
.= (F -- r) /\ (G -- r) by Th60 ; :: thesis: verum