for x being Element of Vars holds
( x <> * & x <> non_op ) ;