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