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:32;
then consider c being set such that
A2: for y being set st y in {a,b} holds
c c= y and
A3: c in X by A1;
take c ; :: thesis: ( c c= a /\ b & c in X )
b in {a,b} by TARSKI:def 2;
then A4: c c= b by A2;
a in {a,b} by TARSKI:def 2;
then c c= a by A2;
hence ( c c= a /\ b & c in X ) by A3, A4, XBOOLE_1:19; :: thesis: verum