let L be non empty reflexive RelStr ; :: thesis: for x being Element of L holds
( {x} is directed & {x} is filtered )
let x be Element of L; :: thesis: ( {x} is directed & {x} is filtered )
set X = {x};

hereby :: according to WAYBEL_0:def 1 :: thesis: {x} is filtered

let z, y be Element of L; :: thesis: ( z in {x} & y in {x} implies ex x being Element of L st
( x in {x} & z <= x & y <= x ) )
assume that
A1: z in {x} and
A2: y in {x} ; :: thesis: ex x being Element of L st
( x in {x} & z <= x & y <= x )
take x = x; :: thesis: ( x in {x} & z <= x & y <= x )
thus ( x in {x} & z <= x & y <= x ) by A1, A2, TARSKI:def 1; :: thesis: verum

end;

hereby :: according to WAYBEL_0:def 2 :: thesis: verum

let z, y be Element of L; :: thesis: ( z in {x} & y in {x} implies ex x being Element of L st
( x in {x} & x <= z & x <= y ) )
assume that
A3: z in {x} and
A4: y in {x} ; :: thesis: ex x being Element of L st
( x in {x} & x <= z & x <= y )
take x = x; :: thesis: ( x in {x} & x <= z & x <= y )
thus ( x in {x} & x <= z & x <= y ) by A3, A4, TARSKI:def 1; :: thesis: verum

end;