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