let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { [i,j,k] where i, j, k is Element of NAT : ( ( i = j or j = k or k = i ) & i in {1,2,3} & j in {1,2,3} & k in {1,2,3} ) } or x in [:{1,2,3},{1,2,3},{1,2,3}:] )
assume x in { [i,j,k] where i, j, k is Element of NAT : ( ( i = j or j = k or k = i ) & i in {1,2,3} & j in {1,2,3} & k in {1,2,3} ) } ; :: thesis: x in [:{1,2,3},{1,2,3},{1,2,3}:]
then ex i, j, k being Element of NAT st
( x = [i,j,k] & ( i = j or j = k or k = i ) & i in {1,2,3} & j in {1,2,3} & k in {1,2,3} ) ;
hence x in [:{1,2,3},{1,2,3},{1,2,3}:] by MCART_1:69; :: thesis: verum