class TEST1

create
	make

feature

	make
		do
		end

invariant
	fine: (once "Weasel") /= Void
end