set X = [#] L;
thus for x, y being Element of L st x in [#] L & y <= x holds
y in [#] L ; :: according to WAYBEL_0:def 19 :: thesis: [#] L is upper
thus for x, y being Element of L st x in [#] L & x <= y holds
y in [#] L ; :: according to WAYBEL_0:def 20 :: thesis: verum