theorem
  phi[X]
  proof
    thus phi[X];
  end;

theorem
  phi[X] & psi[Y]
  proof
    thus phi[X];
    thus psi[Y];
  end;

theorem
  phi[X] implies psi[X]
  proof
    assume phi[X];
    thus psi[X];
  end;

theorem
  phi[X] iff psi[X]
  proof
    thus phi[X] implies psi[X];
    thus psi[X] implies phi[X];
  end;

theorem
  phi[X] iff psi[X]
  proof
    hereby 
      assume phi[X];
      thus psi[X];
    end;
    assume psi[X];
    thus phi[X];
  end;

theorem
  phi[X] or psi[X]
  proof
    assume not phi[X];
    thus psi[X];
  end;

theorem
  for X being set holds phi[X]
  proof
    let X be set;
    thus phi[X];
  end;

theorem
  ex X being set st phi[X]
  proof
    take X;
    thus phi[X];
  end;