set x = the LowerBound of X;
the LowerBound of X in SetMinorant X by Def15;
hence not SetMinorant X is empty ; :: thesis: verum