(assert
 '(forall (x y z)
    (implies
      (and
        (part-of x y)
        (part-of y z)
      )
      (part-of x z)
  ) )
:name '1point1point1)

(assert
 '(forall (x y alpha t)
    (exists (z arb-part)
      (implies
        (and
          (and
            (member t alpha)
            (part-of t x)
          ) ; alpha is included in the parts of x -> for all t which are members of alpha, t is a part of x
          (implies
            (part-of y x)
            (and
              (member z alpha)
              (and
                (part-of arb-part z)
                (part-of arb-part y)
        ) ) ) )
        (sum-of x alpha)
  ) ) )
:name '1point1point2)

(assert
 '(forall (alpha)
    (exists (arb-member sum)
      (implies
        (member arb-member alpha)
        (sum-of sum alpha) ; there exists a sum ('sum') of alpha
  ) ) )
:name '1point1point3)

(prove
 '(forall (x)
    (part-of x x)
  )
:name '1point1point4)