reconsider
A
=
C
,
B
=
D
as
Subset
of
T
;
A1
:
A
is
open
by
Th1
;
A2
:
B
is
open
by
Th1
;
A3
:
A
is
closed
by
Th2
;
A4
:
B
is
closed
by
Th2
;
A
\/
B
is
open
by
A1
,
A2
;
hence
C
\/
D
is
Element
of
OpenClosedSet
T
by
A3
,
A4
,
Th3
;
:: thesis:
verum