let F, G, H be ext-real-membered set ; :: thesis: F -- (G \/ H) = (F -- G) \/ (F -- H)
thus F -- (G \/ H) = F ++ ((-- G) \/ (-- H)) by Th5
.= (F -- G) \/ (F -- H) by Th41 ; :: thesis: verum