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