let S be Subset of R; :: thesis: ( S is empty implies ( S is lower & S is upper ) )
assume S is empty ; :: thesis: ( S is lower & S is upper )
then X: S = {} R ;
hence for x, y being Element of R st x in S & y <= x holds
y in S ; :: according to WAYBEL_0:def 19 :: thesis: S is upper
thus for x, y being Element of R st x in S & x <= y holds
y in S by X; :: according to WAYBEL_0:def 20 :: thesis: verum