let S be Subset of R; :: thesis: S is upper
ex x being Element of R st the carrier of R = {x} by TEX_1:def 1;
then ( S = {} R or S = [#] R ) by ZFMISC_1:33;
hence S is upper ; :: thesis: verum