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 a, b being Element of L such that
A2: M = [#a,b#] by Def5;
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₁ being Element of the carrier of L st
( b₁ in M & x <= b₁ & y <= b₁ ) )
assume A3: ( x in M & y in M ) ; :: thesis: ex b₁ being Element of the carrier of L st
( b₁ in M & x <= b₁ & y <= b₁ )
take b ; :: thesis: ( b in M & x <= b & y <= b )
consider z being set such that
A4: z in M by A1, XBOOLE_0:def 1;
reconsider z = z as Element of L by A4;
( a <= z & z <= b ) by A2, A4, Def4;
then ( a <= b & b <= b ) by ORDERS_2:26;
hence b in M by A2, Def4; :: thesis: ( x <= b & y <= b )
thus ( x <= b & y <= b ) by A2, A3, Def4; :: thesis: verum