let X be set ; :: thesis: for n, i 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 n, i 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 i', j' being Nat such that
A3: i' in Seg n and
A4: j' in Seg n and
A5: i' < j' and
A6: X = {i',j'} by A1, Th1;

now

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

case i = i' ; :: 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 = j' ; :: 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