consider A being OSSubset of OU0;
OSSubSort A c= OSSubSort OU0 by Th23;
hence not OSSubSort OU0 is empty ; :: thesis: verum