consider x being LowerBound of X;
x in SetMinorant X by Def15;
hence not SetMinorant X is empty ; :: thesis: verum