let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in 3 \ 2 or x in 3 \ 1 )
assume x in 3 \ 2 ; :: thesis: x in 3 \ 1
then x = 2 by Th4, TARSKI:def 1;
hence x in 3 \ 1 by Th3, TARSKI:def 2; :: thesis: verum