per
cases
(
t
in
{
1,2
}
or not
t
in
{
1,2
}
)
;
suppose
t
in
{
1,2
}
;
:: thesis:
IFIN
(
t
,
{
1,2
}
,1,2) is
Element
of
StoppingSetExt
2
hence
IFIN
(
t
,
{
1,2
}
,1,2) is
Element
of
StoppingSetExt
2
by
Lemma1
,
MATRIX_7:def 1
;
:: thesis:
verum
end;
suppose
not
t
in
{
1,2
}
;
:: thesis:
IFIN
(
t
,
{
1,2
}
,1,2) is
Element
of
StoppingSetExt
2
hence
IFIN
(
t
,
{
1,2
}
,1,2) is
Element
of
StoppingSetExt
2
by
Lemma2
,
MATRIX_7:def 1
;
:: thesis:
verum
end;
end;