reconsider E = NAT --> ({} T) as SetSequence of T ;
E is constant ;
hence ex b₁ being SetSequence of T st
( b₁ is constant & not b₁ is empty ) ; :: thesis: verum