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