theorem :: EXCHSORT:18

for a being Ordinal
for A being empty set holds A is a -based ;