let X be set ; :: thesis: 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; :: thesis: ( 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} ) ) :: thesis: ( 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) ; :: thesis: ex i, j being Nat st
( i in Seg n & j in Seg n & i < j & X = {i,j} )
then consider x, y being set 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; :: thesis: verum

end;

assume ex i, j being Nat st
( i in Seg n & j in Seg n & i < j & X = {i,j} ) ; :: thesis: 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; :: thesis: verum