let A be 2 -element set ; :: thesis: for a, b being Element of A st a <> b holds
id A = {[a,a],[b,b]}
let a, b be Element of A; :: thesis: ( a <> b implies id A = {[a,a],[b,b]} )
assume A0: a <> b ; :: thesis: id A = {[a,a],[b,b]}
set c = a;
set d = b;
set x1 = [a,a];
set x2 = [b,b];
T0: A = {a,b} by Lemma3, A0;
T2: id {a,b,a,b} = id {a,a,b,b} by ENUMSET1:62
.= id {a,b,b} by ENUMSET1:31
.= id {b,b,a} by ENUMSET1:59
.= id {a,b} by ENUMSET1:30 ;
{[a,a],[b,b],[a,a],[b,b]} = {[a,a],[a,a],[b,b],[b,b]} by ENUMSET1:62
.= {[a,a],[b,b],[b,b]} by ENUMSET1:31
.= {[b,b],[b,b],[a,a]} by ENUMSET1:59
.= {[a,a],[b,b]} by ENUMSET1:30 ;
hence id A = {[a,a],[b,b]} by NECKLA_3:2, T2, T0; :: thesis: verum