116 |
* of a @misspelled{forall}/exists formula $@dall{x; s_1; @sexists{s_2; P[x; y]}}$, |
* of a @misspelled{forall}/exists formula $@dall{x; s_1; @sexists{s_2; P[x; y]}}$, |

117 |
* there is a set $s_3$ that contains the collection of sets that |
* there is a set $s_3$ that contains the collection of sets that |

118 |
* were chosen by the existential. The reason that the collection is |
* were chosen by the existential. The reason that the collection is |

119 |
* not defined as a set constructor is the the proof of the @misspelled{forall}/exists |
* not defined as a set constructor is that the proof of the @misspelled{forall}/exists |

120 |
* formula is part of the construction. If the set $s_1$ has canonical |
* formula is part of the construction. If the set $s_1$ has canonical |

121 |
* for $s_1 = @collect{x; T; f[x]}$, the proof provides a witness |
* for $s_1 = @collect{x; T; f[x]}$, the proof provides a witness |

122 |
* that inhabits the function space $T @rightarrow @set$. The canonical |
* that inhabits the function space $T @rightarrow @set$. The canonical |