environ == We interpret the predicates Div and Mult as follows: == Div[x,y,z] iff x / y = z == Mult[x,y,z] iff x * y = z reserve x,y,z,t,p for Real; given 0 being Real; A1: for x,y,z st y <> 0 holds Div[x, y, z] iff Mult[z, y, x]; A2: for x,y,z,t holds Div[z, t, x] & Div[z, t, y] iff x=y; A3: ex p st for x holds Mult[x, p, p]; given 1 being Real; A4: 1<>0; A5: for x holds Mult[x, 1, x]; begin absurd: for x holds Mult[0,1,x] proof let x be Real; a1: 0 = 0; a2: Div[x,1,0] by a1, A2; thus thesis by A1, a2, A4; end;