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

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

hence
{ x where x is Element of L : V "/\" {x} c= V } is filtered Subset of L
; :: thesis: verum
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_{1} being Element of the carrier of L st

( b_{1} in G1 & b_{1} <= x & b_{1} <= y ) )

assume x in G1 ; :: thesis: ( not y in G1 or ex b_{1} being Element of the carrier of L st

( b_{1} in G1 & b_{1} <= x & b_{1} <= 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_{1} being Element of the carrier of L st

( b_{1} in G1 & b_{1} <= x & b_{1} <= 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

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

end;( b

assume x in G1 ; :: thesis: ( not y in G1 or ex b

( b

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

( b

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

hence
z in G1
; :: thesis: ( z <= x & z <= y )
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;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

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