reconsider A = {0,1,2,3} as non empty set ;
take A ; :: thesis: ex x1, x2, x3, x4 being Element of A st
( A = {x1,x2,x3,x4} & x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4 )
reconsider x1 = 0 , x2 = 1, x3 = 2, x4 = 3 as Element of A by ENUMSET1:def 2;
take x1 ; :: thesis: ex x2, x3, x4 being Element of A st
( A = {x1,x2,x3,x4} & x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4 )
take x2 ; :: thesis: ex x3, x4 being Element of A st
( A = {x1,x2,x3,x4} & x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4 )
take x3 ; :: thesis: ex x4 being Element of A st
( A = {x1,x2,x3,x4} & x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4 )
take x4 ; :: thesis: ( A = {x1,x2,x3,x4} & x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4 )
thus ( A = {x1,x2,x3,x4} & x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4 ) ; :: thesis: verum