let A be non trivial set ; :: thesis: ex a, b being Element of A st a <> b
set x = the Element of A;
consider d1 being object such that
A1: ( d1 in A & d1 <> the Element of A ) by SUBSET_1:48;
thus ex a, b being Element of A st a <> b by A1; :: thesis: verum