let L be Semilattice; :: thesis: for F being filtered upper Subset of L holds F "/\" F = F
let F be filtered upper Subset of L; :: thesis: F "/\" F = F
thus F "/\" F c= F :: according to XBOOLE_0:def 10 :: thesis: F c= F "/\" F

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in F "/\" F or x in F )
assume x in F "/\" F ; :: thesis: x in F
then consider y, z being Element of L such that
A1: x = y "/\" z and
A2: ( y in F & z in F ) ;
consider t being Element of L such that
A3: t in F and
A4: ( t <= y & t <= z ) by A2, WAYBEL_0:def 2;
y "/\" z >= t by A4, YELLOW_0:23;
hence x in F by A1, A3, WAYBEL_0:def 20; :: thesis: verum

end;

thus F c= F "/\" F by YELLOW_4:40; :: thesis: verum