We want to prove
( S1
S2
: Set
)
neg(S1 U S2) = neg(S1) & neg(S2)
and
( S1
S2
: Set
)
neg(S1 & S2) = neg(S1) U neg(S2) .
Conjunction elimination yields 2 subgoals:
-
(
S1
S2
: Set
)
neg(S1 U S2) = neg(S1) & neg(S2)
-
(
S1
S2
: Set
)
neg(S1 & S2) = neg(S1) U neg(S2)
And thus the main goal is proved.
|