thus {} L is directed :: thesis: {} L is filtered

proof

let x be Element of L; :: according to WAYBEL_0:def 1 :: thesis: for y being Element of L st x in {} L & y in {} L holds
ex z being Element of L st
( z in {} L & x <= z & y <= z )
thus for y being Element of L st x in {} L & y in {} L holds
ex z being Element of L st
( z in {} L & x <= z & y <= z ) ; :: thesis: verum

end;

let x be Element of L; :: according to WAYBEL_0:def 2 :: thesis: for y being Element of L st x in {} L & y in {} L holds
ex z being Element of L st
( z in {} L & z <= x & z <= y )
thus for y being Element of L st x in {} L & y in {} L holds
ex z being Element of L st
( z in {} L & z <= x & z <= y ) ; :: thesis: verum