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};

( {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;( 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

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;( 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