Description: Half-open sets with equal endpoints are empty. (Contributed by Stefan O'Rear, 15-Aug-2015) (Revised by Mario Carneiro, 29-Sep-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | fzo0 | |- ( A ..^ A ) = (/) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fzonel | |- -. A e. ( A ..^ A ) |
|
2 | fzon0 | |- ( ( A ..^ A ) =/= (/) <-> A e. ( A ..^ A ) ) |
|
3 | 2 | necon1bbii | |- ( -. A e. ( A ..^ A ) <-> ( A ..^ A ) = (/) ) |
4 | 1 3 | mpbi | |- ( A ..^ A ) = (/) |