class interface WIN_EVENT

invariant
   good_window: window /= Void;

end of WIN_EVENT