let X be set ; :: thesis: for i, n being Nat st X in 2Set (Seg n) & i in X holds
( i in Seg n & ex j being Nat st
( j in Seg n & i <> j & X = {i,j} ) )
let i, n be Nat; :: thesis: ( X in 2Set (Seg n) & i in X implies ( i in Seg n & ex j being Nat st
( j in Seg n & i <> j & X = {i,j} ) ) )
assume that
A1: X in 2Set (Seg n) and
A2: i in X ; :: thesis: ( i in Seg n & ex j being Nat st
( j in Seg n & i <> j & X = {i,j} ) )
consider i9, j9 being Nat such that
A3: i9 in Seg n and
A4: j9 in Seg n and
A5: i9 < j9 and
A6: X = {i9,j9} by A1, Th1;

now :: thesis: ( ( i = i9 & i in Seg n & ex j being Nat st
( j in Seg n & i <> j & X = {i,j} ) ) or ( i = j9 & i in Seg n & ex j being Nat st
( j in Seg n & i <> j & X = {i,j} ) ) )

per cases ( i = i9 or i = j9 ) by A2, A6, TARSKI:def 2;

case i = i9 ; :: thesis: ( i in Seg n & ex j being Nat st
( j in Seg n & i <> j & X = {i,j} ) )

hence ( i in Seg n & ex j being Nat st
( j in Seg n & i <> j & X = {i,j} ) ) by A3, A4, A5, A6; :: thesis: verum

end;

case i = j9 ; :: thesis: ( i in Seg n & ex j being Nat st
( j in Seg n & i <> j & X = {i,j} ) )

hence ( i in Seg n & ex j being Nat st
( j in Seg n & i <> j & X = {i,j} ) ) by A3, A4, A5, A6; :: thesis: verum

end;

end;

end;

hence ( i in Seg n & ex j being Nat st
( j in Seg n & i <> j & X = {i,j} ) ) ; :: thesis: verum