let A, e be set ; ( e in TWOELEMENTSETS A iff ( e is finite Subset of A & ex x, y being object st
( x in A & y in A & x <> y & e = {x,y} ) ) )
hereby ( e is finite Subset of A & ex x, y being object st
( x in A & y in A & x <> y & e = {x,y} ) implies e in TWOELEMENTSETS A )
assume
e in TWOELEMENTSETS A
;
( e is finite Subset of A & ex x, y being object st
( x in A & y in A & x <> y & e = {x,y} ) )then A1:
ex
z being
Subset of
A st
(
e = z &
card z = 2 )
;
then reconsider e9 =
e as
finite Subset of
A ;
thus
e is
finite Subset of
A
by A1;
ex x, y being object st
( x in A & y in A & x <> y & e = {x,y} )consider x,
y being
object such that A2:
x <> y
and A3:
e9 = {x,y}
by A1, CARD_2:60;
take x =
x;
ex y being object st
( x in A & y in A & x <> y & e = {x,y} )take y =
y;
( x in A & y in A & x <> y & e = {x,y} )
(
x in e9 &
y in e9 )
by A3, TARSKI:def 2;
hence
(
x in A &
y in A )
;
( x <> y & e = {x,y} )thus
(
x <> y &
e = {x,y} )
by A2, A3;
verum
end;
assume that
e is finite Subset of A
and
A4:
ex x, y being object st
( x in A & y in A & x <> y & e = {x,y} )
; e in TWOELEMENTSETS A
consider x, y being Element of A such that
A5:
x in A
and
y in A
and
A6:
not x = y
and
A7:
e = {x,y}
by A4;
reconsider xy = {x,y} as finite Subset of A by A5, ZFMISC_1:32;
ex z being finite Subset of A st
( e = z & card z = 2 )
hence
e in TWOELEMENTSETS A
; verum