| (1) | $X$ is a D666: Transitive set |
| (2) | ${\in}_X$ is the D1943: Membership relation on $X$ |
| (3) | $P$ is a D1124: Well-ordered set |
| ▼ | Set of symbols |
| ▼ | Alphabet |
| ▼ | Deduction system |
| ▼ | Theory |
| ▼ | Zermelo-Fraenkel set theory |
| ▼ | Set |
| ▼ | Transitive set |
| (1) | $X$ is a D666: Transitive set |
| (2) | ${\in}_X$ is the D1943: Membership relation on $X$ |
| (3) | $P$ is a D1124: Well-ordered set |
| ▶ | D686: Class of ordinal numbers |