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;