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