let X be set ; for n being Nat holds
( X in 2Set (Seg n) iff ex i, j being Nat st
( i in Seg n & j in Seg n & i < j & X = {i,j} ) )
let n be Nat; ( X in 2Set (Seg n) iff ex i, j being Nat st
( i in Seg n & j in Seg n & i < j & X = {i,j} ) )
thus
( X in 2Set (Seg n) implies ex i, j being Nat st
( i in Seg n & j in Seg n & i < j & X = {i,j} ) )
( ex i, j being Nat st
( i in Seg n & j in Seg n & i < j & X = {i,j} ) implies X in 2Set (Seg n) )proof
assume
X in 2Set (Seg n)
;
ex i, j being Nat st
( i in Seg n & j in Seg n & i < j & X = {i,j} )
then consider x,
y being
object such that A1:
x in Seg n
and A2:
y in Seg n
and A3:
x <> y
and A4:
X = {x,y}
by SGRAPH1:8;
reconsider x =
x,
y =
y as
Element of
NAT by A1, A2;
(
x > y or
y > x )
by A3, XXREAL_0:1;
hence
ex
i,
j being
Nat st
(
i in Seg n &
j in Seg n &
i < j &
X = {i,j} )
by A1, A2, A4;
verum
end;
assume
ex i, j being Nat st
( i in Seg n & j in Seg n & i < j & X = {i,j} )
; X in 2Set (Seg n)
then consider i, j being Nat such that
A5:
i in Seg n
and
A6:
j in Seg n
and
A7:
i < j
and
A8:
X = {i,j}
;
{i,j} c= Seg n
by A5, A6, ZFMISC_1:32;
hence
X in 2Set (Seg n)
by A5, A6, A7, A8, SGRAPH1:8; verum