diff --git a/2017-12-Birmingham/Part5_Set_Level_Mathematics/set_level_mathematics_exercises.v b/2017-12-Birmingham/Part5_Set_Level_Mathematics/set_level_mathematics_exercises.v
index b7d4014..08e1b5d 100644
--- a/2017-12-Birmingham/Part5_Set_Level_Mathematics/set_level_mathematics_exercises.v
+++ b/2017-12-Birmingham/Part5_Set_Level_Mathematics/set_level_mathematics_exercises.v
@@ -214,7 +214,11 @@ Definition isrefl {X : UU} (R : hrel X) : UU
 (* FILL IN THE DEFINITIONS OF istrans AND issymm *)
 (* Definition istrans {X : UU} (R : hrel X) : UU := *)
 (* Definition issymm {X : UU} (R : hrel X) : UU := *)
-Variables istrans issymm: forall {X: UU}, hrel X -> UU. (* to be deleted *)
+
+Definition istrans {X : UU} (R : hrel X) : UU.
+Admitted.
+Definition issymm {X : UU} (R : hrel X) : UU.
+Admitted.
 
 Definition ispreorder {X : UU} (R : hrel X) : UU := istrans R × isrefl R.