let L be transitive antisymmetric with_infima RelStr ; :: thesis: for V being Subset of L holds { x where x is Element of L : V "/\" {x} c= V } is filtered Subset of L
let V be Subset of L; :: thesis: { x where x is Element of L : V "/\" {x} c= V } is filtered Subset of L
reconsider G1 = { x where x is Element of L : V "/\" {x} c= V } as Subset of L by Lm2;
G1 is filtered

proof

let x, y be Element of L; :: according to WAYBEL_0:def 2 :: thesis: ( not x in G1 or not y in G1 or ex b₁ being Element of the carrier of L st
( b₁ in G1 & b₁ <= x & b₁ <= y ) )
assume x in G1 ; :: thesis: ( not y in G1 or ex b₁ being Element of the carrier of L st
( b₁ in G1 & b₁ <= x & b₁ <= y ) )
then consider x1 being Element of L such that
A1: x = x1 and
A2: V "/\" {x1} c= V ;
assume y in G1 ; :: thesis: ex b₁ being Element of the carrier of L st
( b₁ in G1 & b₁ <= x & b₁ <= y )
then consider y1 being Element of L such that
A3: y = y1 and
A4: V "/\" {y1} c= V ;
take z = x1 "/\" y1; :: thesis: ( z in G1 & z <= x & z <= y )
V "/\" {z} c= V

proof

A5: {z} "/\" V = { (z "/\" v) where v is Element of L : v in V } by YELLOW_4:42;
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in V "/\" {z} or q in V )
assume q in V "/\" {z} ; :: thesis: q in V
then consider v being Element of L such that
A6: q = z "/\" v and
A7: v in V by A5;
A8: ( {x1} "/\" V = { (x1 "/\" s) where s is Element of L : s in V } & q = x1 "/\" (y1 "/\" v) ) by A6, LATTICE3:16, YELLOW_4:42;
{y1} "/\" V = { (y1 "/\" t) where t is Element of L : t in V } by YELLOW_4:42;
then y1 "/\" v in V "/\" {y1} by A7;
then q in V "/\" {x1} by A4, A8;
hence q in V by A2; :: thesis: verum

end;

hence z in G1 ; :: thesis: ( z <= x & z <= y )
thus ( z <= x & z <= y ) by A1, A3, YELLOW_0:23; :: thesis: verum

end;

hence { x where x is Element of L : V "/\" {x} c= V } is filtered Subset of L ; :: thesis: verum