--- /dev/null
+# The term \Omega
+# This book is not valid in AUT-QE because [y:'type'] is not allowed
+# This book is not valid in \lambda\delta < 3 because sort inclusion is not allowed
+# This book is not valid in \lambda\delta 3 because of two \upsilon-reductions on layer 1
+
++l
+@ Delta := [x:[y:'type']'type']<x>x : [x:[y:'type']'type']'type'
+ Omega := <Delta>Delta : 'type'
+-l