let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {[1,1,1]} or x in [:{1},{1},{1}:] )
assume x in {[1,1,1]} ; :: thesis: x in [:{1},{1},{1}:]
then x = [1,1,1] by TARSKI:def 1;
hence x in [:{1},{1},{1}:] by Lm1, MCART_1:69; :: thesis: verum