let S be Subset of L; :: thesis: ( S is empty implies ( S is directed & S is filtered ) )
assume S is empty ; :: thesis: ( S is directed & S is filtered )
then A1: S = {} L ;
thus S is directed :: thesis: S 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 S & y in S holds
ex z being Element of L st
( z in S & x <= z & y <= z )
thus for y being Element of L st x in S & y in S holds
ex z being Element of L st
( z in S & x <= z & y <= z ) by A1; :: 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 S & y in S holds
ex z being Element of L st
( z in S & z <= x & z <= y )
thus for y being Element of L st x in S & y in S holds
ex z being Element of L st
( z in S & z <= x & z <= y ) by A1; :: thesis: verum