set X = [#] L;
let x, y be Element of L; :: according to WAYBEL_0:def 2 :: thesis: ( x in [#] L & y in [#] L implies ex z being Element of L st
( z in [#] L & z <= x & z <= y ) )
assume that
x in [#] L and
y in [#] L ; :: thesis: ex z being Element of L st
( z in [#] L & z <= x & z <= y )
consider z being Element of L such that
A1: z is_<=_than [#] L by YELLOW_0:def 4;
take z ; :: thesis: ( z in [#] L & z <= x & z <= y )
thus ( z in [#] L & z <= x & z <= y ) by A1; :: thesis: verum