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 & y in Seg n & x <> y & X = {x,y} ) by SGRAPH1:10;
reconsider x = x, y = y as Element of NAT by A1;
( x > y or y > x ) by A1, 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; :: 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
A2: ( i in Seg n & j in Seg n & i < j & X = {i,j} ) ;
{i,j} c= Seg n by A2, ZFMISC_1:38;
hence X in 2Set (Seg n) by A2, SGRAPH1:10; :: thesis: verum