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