let A be 2 -element set ; for a, b being Element of A st a <> b holds
id A = {[a,a],[b,b]}
let a, b be Element of A; ( a <> b implies id A = {[a,a],[b,b]} )
assume A0:
a <> b
; 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; verum