now

let x be set ; :: thesis: ( 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} ) } implies 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:73; :: thesis: verum

end;

hence { [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} ) } c= [:{1,2,3},{1,2,3},{1,2,3}:] by TARSKI:def 3; :: thesis: verum