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

let x, y be Element of L; :: according to WAYBEL_0:def 2 :: thesis:
assume x in G1 ; :: thesis:
then consider x1 being Element of L such that
A1: x = x1 and
A2: V "/\" {x1} c= V ;
assume y in G1 ; :: thesis:
then consider y1 being Element of L such that
A3: y = y1 and
A4: V "/\" {y1} c= V ;
take z = x1 "/\" y1; :: thesis:
V "/\" {z} c= V

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:
assume q in V "/\" {z} ; :: thesis:
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:

end;

end;