proptest : THEORY

BEGIN

  A,B,C : bool            % -- einige aussagenlogische Symbole

  thm : THEOREM
    (A IMPLIES (B IMPLIES C))
      AND
    (A IMPLIES B) 
      AND 
    A
    IMPLIES C

  thm_2 : THEOREM
       (A => (B => C)) & (A => B) & A 
    => C

END proptest