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

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

thus
F c= F "/\" F
by YELLOW_4:40; :: thesis: verum
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;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