let X be Subset of L; :: thesis: ( X is directed & X is filtered )
thus X is directed :: thesis: X is filtered

proof

let x, y be Element of L; :: according to WAYBEL_0:def 1 :: thesis: ( not x in X or not y in X or ex b₁ being Element of the carrier of L st
( b₁ in X & x <= b₁ & y <= b₁ ) )
( ( x <= y & y <= y ) or ( x >= x & x >= y ) ) by WAYBEL_0:def 29;
hence ( not x in X or not y in X or ex b₁ being Element of the carrier of L st
( b₁ in X & x <= b₁ & y <= b₁ ) ) ; :: thesis: verum

end;

let x, y be Element of L; :: according to WAYBEL_0:def 2 :: thesis: ( not x in X or not y in X or ex b₁ being Element of the carrier of L st
( b₁ in X & b₁ <= x & b₁ <= y ) )
( ( x >= y & y <= y ) or ( x >= x & x <= y ) ) by WAYBEL_0:def 29;
hence ( not x in X or not y in X or ex b₁ being Element of the carrier of L st
( b₁ in X & b₁ <= x & b₁ <= y ) ) ; :: thesis: verum