let M be Subset of L; :: thesis: ( not M is empty & M is interval implies M is filtered )
assume A8: ( not M is empty & M is interval ) ; :: thesis: M is filtered
then consider z being object such that
A9: z in M ;
reconsider z = z as Element of L by A9;
consider a, b being Element of L such that
A10: M = [#a,b#] by A8;
A11: z <= b by A10, A9, Def4;
a <= z by A10, A9, Def4;
then A12: a <= b by A11, ORDERS_2:3;
let x, y be Element of L; :: according to WAYBEL_0:def 2 :: thesis: ( not x in M or not y in M or ex b₁ being Element of the carrier of L st
( b₁ in M & b₁ <= x & b₁ <= y ) )
assume that
A13: x in M and
A14: y in M ; :: thesis: ex b₁ being Element of the carrier of L st
( b₁ in M & b₁ <= x & b₁ <= y )
take a ; :: thesis: ( a in M & a <= x & a <= y )
a <= a ;
hence a in M by A10, A12, Def4; :: thesis: ( a <= x & a <= y )
thus ( a <= x & a <= y ) by A10, A13, A14, Def4; :: thesis: verum