What to do

1. Consider how to sketch the proof skeletons for the following theorems:
   • theorem
        for A being Subset of REAL such that 0 is an Element of A
          and for x being an Element of REAL such that x is an
          Element of A holds x + 1 is an Element of A holds NAT
          is a Subset of A

   • theorem
        let X, Y, Z be sets;
        X = bool Y iff for Z being set holds Z is an Element of X
          iff Z is a Subset of Y

   • theorem
        for f1, f2 being Functions of X, Y such that
          Y < > empty set and for x such that x
          is an Element of X holds f1.x = f2.x holds f1=f2