let n be Nat; :: thesis: ( n >= 2 implies {1,2} in 2Set (Seg n) )
assume A1: n >= 2 ; :: thesis: {1,2} in 2Set (Seg n)
1 <= n by A1, XXREAL_0:2;
then A2: 1 in Seg n ;
2 in Seg n by A1;
hence {1,2} in 2Set (Seg n) by A2, Th1; :: thesis: verum