let M be Subset of L; :: thesis: ( not M is empty & M is interval implies M is directed )

assume A1: ( not M is empty & M is interval ) ; :: thesis: M is directed

then consider z being object such that

A2: z in M ;

reconsider z = z as Element of L by A2;

consider a, b being Element of L such that

A3: M = [#a,b#] by A1;

A4: z <= b by A3, A2, Def4;

a <= z by A3, A2, Def4;

then A5: a <= b by A4, ORDERS_2:3;

let x, y be Element of L; :: according to WAYBEL_0:def 1 :: thesis: ( not x in M or not y in M or ex b_{1} being Element of the carrier of L st

( b_{1} in M & x <= b_{1} & y <= b_{1} ) )

assume that

A6: x in M and

A7: y in M ; :: thesis: ex b_{1} being Element of the carrier of L st

( b_{1} in M & x <= b_{1} & y <= b_{1} )

take b ; :: thesis: ( b in M & x <= b & y <= b )

b <= b ;

hence b in M by A3, A5, Def4; :: thesis: ( x <= b & y <= b )

thus ( x <= b & y <= b ) by A3, A6, A7, Def4; :: thesis: verum

assume A1: ( not M is empty & M is interval ) ; :: thesis: M is directed

then consider z being object such that

A2: z in M ;

reconsider z = z as Element of L by A2;

consider a, b being Element of L such that

A3: M = [#a,b#] by A1;

A4: z <= b by A3, A2, Def4;

a <= z by A3, A2, Def4;

then A5: a <= b by A4, ORDERS_2:3;

let x, y be Element of L; :: according to WAYBEL_0:def 1 :: thesis: ( not x in M or not y in M or ex b

( b

assume that

A6: x in M and

A7: y in M ; :: thesis: ex b

( b

take b ; :: thesis: ( b in M & x <= b & y <= b )

b <= b ;

hence b in M by A3, A5, Def4; :: thesis: ( x <= b & y <= b )

thus ( x <= b & y <= b ) by A3, A6, A7, Def4; :: thesis: verum