sig Universum {
	o: Universum set -> set Universum // (x->z->y in o) <=> (x*y = z) <=> (x.o.y = z)
}{}

one sig e in Universum {}{}

pred H {
	// Closure: x*y = z
	all x,y:Universum | some x.o.y

	// Associativity: (x*y)*z = x*(y*z)
	all x,y,z:Universum | (x.o.y).o.z = x.o.(y.o.z)

	// Identity: x*e = x = e*x
	all x:Universum | (x.o.e = x) and (e.o.x = x)

	// Inverse: x*y = e = y*x
	all x:Universum | some y:Universum | (x.o.y = e) and (y.o.x = e)
}

run H for 3 Universum