Let \(i_{1},i_{2}:\mathord {\textnormal {\textsf {Level}}}\). Then \(i_{1}\le i_{2}\) is a propositional judgment form.