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