thus for x, y being Element of R st x in {} R & y <= x holds
y in {} R ; :: according to WAYBEL_0:def 19 :: thesis: {} R is upper
thus for x, y being Element of R st x in {} R & x <= y holds
y in {} R ; :: according to WAYBEL_0:def 20 :: thesis: verum