let x be set ; :: thesis: ( {x} is c=directed & {x} is c=filtered )
set X = {x};
hereby :: according to COHSP_1:def 4 :: thesis: {x} is c=filtered
let Y be finite Subset of {x}; :: thesis: ex x being set st
( union Y c= x & x in {x} )
take x = x; :: thesis: ( union Y c= x & x in {x} )
union Y c= union {x} by ZFMISC_1:77;
hence ( union Y c= x & x in {x} ) by TARSKI:def 1, ZFMISC_1:25; :: thesis: verum
end;
let Y be finite Subset of {x}; :: according to COHSP_1:def 5 :: thesis: ex a being set st
( ( for y being set st y in Y holds
a c= y ) & a in {x} )
take x ; :: thesis: ( ( for y being set st y in Y holds
x c= y ) & x in {x} )
thus for y being set st y in Y holds
x c= y by TARSKI:def 1; :: thesis: x in {x}
thus x in {x} by TARSKI:def 1; :: thesis: verum