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