set X = [#] L;

let x, y be Element of L; :: according to WAYBEL_0:def 1 :: thesis: ( x in [#] L & y in [#] L implies ex z being Element of L st

( z in [#] L & x <= z & y <= z ) )

assume that

x in [#] L and

y in [#] L ; :: thesis: ex z being Element of L st

( z in [#] L & x <= z & y <= z )

consider z being Element of L such that

A1: z is_>=_than [#] L by YELLOW_0:def 5;

take z ; :: thesis: ( z in [#] L & x <= z & y <= z )

thus ( z in [#] L & x <= z & y <= z ) by A1; :: thesis: verum

let x, y be Element of L; :: according to WAYBEL_0:def 1 :: thesis: ( x in [#] L & y in [#] L implies ex z being Element of L st

( z in [#] L & x <= z & y <= z ) )

assume that

x in [#] L and

y in [#] L ; :: thesis: ex z being Element of L st

( z in [#] L & x <= z & y <= z )

consider z being Element of L such that

A1: z is_>=_than [#] L by YELLOW_0:def 5;

take z ; :: thesis: ( z in [#] L & x <= z & y <= z )

thus ( z in [#] L & x <= z & y <= z ) by A1; :: thesis: verum