let
a
,
b
be
set
;
:: thesis:
( not
EQV2
(
a
,
b
) is
empty
iff
XOR2
(
a
,
b
) is
empty
)
( not
EQV2
(
a
,
b
) is
empty
iff ( not
a
is
empty
iff not
b
is
empty
) ) ;
hence
( not
EQV2
(
a
,
b
) is
empty
iff
XOR2
(
a
,
b
) is
empty
) ;
:: thesis:
verum