@ means less numerous than or equally numerous with
# means less numerous than
~ means equinumerous
/x/ means cardinal of x
e means element of
€ means subset of
¥ is the intersection symbol
Theorem: (x @ y)(y @ x) --> x ~ y
x # y --> No bijection exists from x to y; ran(x) ¥ y is non-empty.
So x e T, where T is the class of sets each of which is bijective with x.
So x ~ /x/ e T and /x/ e On U 0. Likewise for y.
From this, we see that
x @ y equiv. to /x/ <= /y/
Now /x/ <= /y/ --> /x/ € of /y/
and likewise for /y/ <= /x/
Thus (x@y)(y@x) -> (/x/ € /y/)(/y/ € /x/) -> /x/ = /y/ -> x ~ y