consider x being UpperBound of X;
x in SetMajorant X by Def14;
hence not SetMajorant X is empty ; :: thesis: verum