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