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 b1 being Element of the carrier of L st
( b1 in X & x <= b1 & y <= b1 ) )
( ( 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 b1 being Element of the carrier of L st
( b1 in X & x <= b1 & y <= b1 ) ) ; :: 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 b1 being Element of the carrier of L st
( b1 in X & b1 <= x & b1 <= 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 b1 being Element of the carrier of L st
( b1 in X & b1 <= x & b1 <= y ) ) ; :: thesis: verum