predtest : THEORY

BEGIN

  T     : TYPE

  x,y,z : VAR T

  P,Q   : [T -> bool]


  predthm : THEOREM
    (FORALL x: P(x) AND Q(x))
    IMPLIES
      (FORALL x: P(x)) 
        AND 
      (FORALL x: Q(x))

  predthm_2 : THEOREM
    (FORALL x: P(x) & Q(x))
    =>
      (FORALL x: P(x)) 
        & 
      (FORALL x: Q(x))


END predtest