reconsider A = {0,1,2} as non empty set ;

take A ; :: thesis: ex x1, x2, x3 being Element of A st

( A = {x1,x2,x3} & x1 <> x2 & x1 <> x3 & x2 <> x3 )

reconsider x1 = 0 , x2 = 1, x3 = 2 as Element of A by ENUMSET1:def 1;

take x1 ; :: thesis: ex x2, x3 being Element of A st

( A = {x1,x2,x3} & x1 <> x2 & x1 <> x3 & x2 <> x3 )

take x2 ; :: thesis: ex x3 being Element of A st

( A = {x1,x2,x3} & x1 <> x2 & x1 <> x3 & x2 <> x3 )

take x3 ; :: thesis: ( A = {x1,x2,x3} & x1 <> x2 & x1 <> x3 & x2 <> x3 )

thus ( A = {x1,x2,x3} & x1 <> x2 & x1 <> x3 & x2 <> x3 ) ; :: thesis: verum

take A ; :: thesis: ex x1, x2, x3 being Element of A st

( A = {x1,x2,x3} & x1 <> x2 & x1 <> x3 & x2 <> x3 )

reconsider x1 = 0 , x2 = 1, x3 = 2 as Element of A by ENUMSET1:def 1;

take x1 ; :: thesis: ex x2, x3 being Element of A st

( A = {x1,x2,x3} & x1 <> x2 & x1 <> x3 & x2 <> x3 )

take x2 ; :: thesis: ex x3 being Element of A st

( A = {x1,x2,x3} & x1 <> x2 & x1 <> x3 & x2 <> x3 )

take x3 ; :: thesis: ( A = {x1,x2,x3} & x1 <> x2 & x1 <> x3 & x2 <> x3 )

thus ( A = {x1,x2,x3} & x1 <> x2 & x1 <> x3 & x2 <> x3 ) ; :: thesis: verum