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;