| Formula |
0\(\href{../symbols/delimiters-brackets.html}{(} \href{../symbols/forall-binder.html}{\forall} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{K} \href{../symbols/typing-colon.html}{:} \href{../symbols/class-type.html}{\mathsf{Class}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/card-op.html}{ \mid } \href{../symbols/variables.html}{K} \href{../symbols/card-op.html}{ \mid } \href{../symbols/eq-pred.html}{=} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/on-const.html}{\mathbf{On}} \href{../symbols/bininter-op.html}{\cap} \href{../symbols/biginter-op.html}{\bigcap} \href{../symbols/class-comprehension.html}{\{} \href{../symbols/variables.html}{a} \href{../symbols/class-comprehension.html}{ \mid } \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{a} \href{../symbols/in-pred.html}{\in} \href{../symbols/on-const.html}{\mathbf{On}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/and-conn.html}{\land} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{K} ≼\href{../symbols/variables.html}{a} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/class-comprehension.html}{\}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \)
|