Grzegorz Bancerek wrote: > And also > not x is not not non irrational, .... Of course, I was wrong. It is incorrect according to Mizar syntax. It may be only one "not" after "is". I was deceived by mizarmode ;-) which writes "No more errors!!" if the cursor is in far position. Grzegorz