environ
        == We interpret the predicates Neg and Square as follows:
        ==         Neg[x,y] iff y = -x
        ==         Square[x,z] iff  x * x = z

reserve x,y,z,t,p for Real;

A1: for x ex z st Neg[x,z];

A2: for x ex z st Square[x,z];

A3: for x, y, z st Neg[x,y] holds Square[x,z] iff Square[y,z];

A4: for x, y, z st Square[x,z] & Square[y,z] holds x = y;

begin

absurd: for x holds Neg[x,x] proof
    let x be Real;
           consider p such that
      B1: Neg[x,p] by A1;
           consider t such that
      B2: Square[x,t] by A2;
       1: Square[x,t] iff Square[p,t] by B1, A3;
       2: Square[x,t] & Square[p,t] by B2, 1;
       3: x=p by 2, A4;
    thus thesis by B1, 3;
end;