for n being Nat st n >= 2 holds
{1,2} in 2Set (Seg n)