let M be Subset of L; :: thesis: ( not M is empty & M is interval implies M is filtered )
assume A5: ( not M is empty & M is interval ) ; :: thesis: M is filtered
then consider a, b being Element of L such that
A6: M = [#a,b#] by Def5;
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 A7: ( x in M & 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 )
consider z being set such that
A8: z in M by A5, XBOOLE_0:def 1;
reconsider z = z as Element of L by A8;
( a <= z & z <= b ) by A6, A8, Def4;
then ( a <= a & a <= b ) by ORDERS_2:26;
hence a in M by A6, Def4; :: thesis: ( a <= x & a <= y )
thus ( a <= x & a <= y ) by A6, A7, Def4; :: thesis: verum