let A be 2 -element set ; :: thesis: for a, b being Element of A st a <> b holds
A = {a,b}
let a, b be Element of A; :: thesis: ( a <> b implies A = {a,b} )
assume A0: a <> b ; :: thesis: A = {a,b}
card A = 2 by CARD_1:def 7;
then consider c, d being object such that
A1: ( c <> d & A = {c,d} ) by CARD_2:60;
( a = c or a = d ) by TARSKI:def 2, A1;
hence A = {a,b} by A0, TARSKI:def 2, A1; :: thesis: verum