Description: Caratheodory measurable sets are subsets of the universe. (Contributed by Thierry Arnoux, 21-May-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | carsgval.1 | ||
carsgval.2 | |||
difelcarsg.1 | |||
Assertion | elcarsgss |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | carsgval.1 | ||
2 | carsgval.2 | ||
3 | difelcarsg.1 | ||
4 | 1 2 | carsgcl | |
5 | 4 3 | sseldd | |
6 | 5 | elpwid |