let X be set ; :: thesis: ( X is c=filtered implies for a, b being set st a in X & b in X holds
ex c being set st
( c c= a /\ b & c in X ) )
assume A1: for Y being finite Subset of X ex a being set st
( ( for y being set st y in Y holds
a c= y ) & a in X ) ; :: according to COHSP_1:def 5 :: thesis: for a, b being set st a in X & b in X holds
ex c being set st
( c c= a /\ b & c in X )
let a, b be set ; :: thesis: ( a in X & b in X implies ex c being set st
( c c= a /\ b & c in X ) )
assume ( a in X & b in X ) ; :: thesis: ex c being set st
( c c= a /\ b & c in X )
then {a,b} c= X by ZFMISC_1:38;
then consider c being set such that
A2: ( ( for y being set st y in {a,b} holds
c c= y ) & c in X ) by A1;
take c ; :: thesis: ( c c= a /\ b & c in X )
( a in {a,b} & b in {a,b} ) by TARSKI:def 2;
then ( c c= a & c c= b ) by A2;
hence ( c c= a /\ b & c in X ) by A2, XBOOLE_1:19; :: thesis: verum