let x be object ; TARSKI:def 3 ( 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} ) }
; 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; verum