Z notation

Hi

The problem im having is

I have a school which is made up of Instructors & Pupils,

A Pupil can only be in one lesson at any given time.

Im not sure how do I express this in Z?

Do I inteduce variables say Max_Lesons_At_Given_Date_Time, and Lessons_At_GivenDate_Time_Per_Pupil.

And say something like:

Max_Lesons_At_Given_Date_Time = 1

#Lessons_At_GivenDate_Time_Per_Pupil ≤ Max_Lesons_At_Given_Date_Time

Or do I just use one and say:

# Lessons_At_GivenDate_Time_Per_Pupil ≤ 1

Any ideas thanks