let x, y be set ; {x,y,(x /\ y)} is c=filtered
let A be finite Subset of {x,y,(x /\ y)}; COHSP_1:def 5 ex a being set st
( ( for y being set st y in A holds
a c= y ) & a in {x,y,(x /\ y)} )
take a = x /\ y; ( ( for y being set st y in A holds
a c= y ) & a in {x,y,(x /\ y)} )
hereby a in {x,y,(x /\ y)}
end;
thus
a in {x,y,(x /\ y)}
by ENUMSET1:def 1; verum