let t be set ; :: thesis: ( t in [:(A \ {(In 0 ,2)}),(A \ {(In 0 ,2)}):] implies mult_2 . t in A \ {(In 0 ,2)} )
assume t in [:(A \ {(In 0 ,2)}),(A \ {(In 0 ,2)}):] ; :: thesis: mult_2 . t in A \ {(In 0 ,2)}
then t = [(In 1,2),(In 1,2)] by Lm20, TARSKI:def 1;
hence mult_2 . t in A \ {(In 0 ,2)} by Lm18, Lm19, TARSKI:def 1; :: thesis: verum