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