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₁ being Element of the carrier of L st
( b₁ in M & x <= b₁ & y <= b₁ ) )
assume that
A6: x in M and
A7: 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 )
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