Write and check with Mizar the proof skeletons for the following.

1. Use environ block from TARSKI (for newer libraries, use MBOOLEAN) to create the proof skeleton for:

   reserve X, Y, Z for set;

   theorem
      X = bool Y iff for Z holds Z in X iff Z c= Y;

2. Use environ block from AXIOMS to create the proof skeleton for:

   reserve x, y, z for Element of REAL;

   theorem
      for A being Subset of REAL st 0 in A & for x st x in A holds x + 1 in A holds NAT c= A;

3. Use environ block from FUNCT_2 FUNCT_3 to create the proof skeleton for:

   reserve X, Y for set, x for object;

   theorem
      for f1, f2 being Function of X, Y st Y <> { }
        & for x st x in X holds f1.x = f2.x
        holds f1 = f2;

[ Back ]