let S be Subset of R; :: thesis: S is upper
consider x being Element of R such that
A1: the carrier of R = {x} by TEX_1:def 1;
( S = {} R or S = [#] R ) by A1, ZFMISC_1:39;
hence S is upper ; :: thesis: verum