{} P in { X where X is Subset of P : X is lower } ;
hence { X where X is Subset of P : X is lower } is non empty set ; :: thesis: verum