let x, y be set ; :: thesis: {x,y,(x /\ y)} is c=filtered
let A be finite Subset of {x,y,(x /\ y)}; :: according to COHSP_1:def 5 :: thesis: 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; :: thesis: ( ( for y being set st y in A holds
a c= y ) & a in {x,y,(x /\ y)} )
hereby :: thesis: a in {x,y,(x /\ y)}
let b be set ; :: thesis: ( b in A implies a c= b )
assume b in A ; :: thesis: a c= b
then ( b = x or b = y or b = x /\ y ) by ENUMSET1:def 1;
hence a c= b by XBOOLE_1:17; :: thesis: verum
end;
thus a in {x,y,(x /\ y)} by ENUMSET1:def 1; :: thesis: verum