theorem :: FOMODEL0:30

for x being set
for D being non empty set holds
( x in (D *) \ {{}} iff ( x is b₂ -valued FinSequence & not x is empty ) )