let L be Lattice; :: thesis: for H, F being Filter of L holds <.(F \/ H).) = { r where r is Element of L : ex p, q being Element of L st
( p "/\" q [= r & p in F & q in H ) }
let H, F be Filter of L; :: thesis: <.(F \/ H).) = { r where r is Element of L : ex p, q being Element of L st
( p "/\" q [= r & p in F & q in H ) }
set X = { r1 where r1 is Element of L : ex p, q being Element of L st
( p "/\" q [= r1 & p in F & q in H ) } ;
consider p1 being Element of L such that
A1: p1 in F by SUBSET_1:4;
consider q1 being Element of L such that
A2: q1 in H by SUBSET_1:4;
p1 "/\" q1 in { r1 where r1 is Element of L : ex p, q being Element of L st
( p "/\" q [= r1 & p in F & q in H ) } by A1, A2;
then reconsider D = { r1 where r1 is Element of L : ex p, q being Element of L st
( p "/\" q [= r1 & p in F & q in H ) } as non empty set ;
D c= the carrier of L

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in D or x in the carrier of L )
assume x in D ; :: thesis: x in the carrier of L
then ex r1 being Element of L st
( x = r1 & ex p, q being Element of L st
( p "/\" q [= r1 & p in F & q in H ) ) ;
hence x in the carrier of L ; :: thesis: verum

end;

then reconsider D = D as non empty Subset of L ;
A3: for p, q being Element of L st p in D & p [= q holds
q in D

proof

let p, q be Element of L; :: thesis: ( p in D & p [= q implies q in D )
assume p in D ; :: thesis: ( not p [= q or q in D )
then ex r1 being Element of L st
( p = r1 & ex p, q being Element of L st
( p "/\" q [= r1 & p in F & q in H ) ) ;
then consider p1, q1 being Element of L such that
A4: p1 "/\" q1 [= p and
A5: ( p1 in F & q1 in H ) ;
assume p [= q ; :: thesis: q in D
then p1 "/\" q1 [= q by A4, LATTICES:7;
hence q in D by A5; :: thesis: verum

end;

for p, q being Element of L st p in D & q in D holds
p "/\" q in D

proof

let p, q be Element of L; :: thesis: ( p in D & q in D implies p "/\" q in D )
assume p in D ; :: thesis: ( not q in D or p "/\" q in D )
then ex r1 being Element of L st
( p = r1 & ex p, q being Element of L st
( p "/\" q [= r1 & p in F & q in H ) ) ;
then consider p1, q1 being Element of L such that
A6: p1 "/\" q1 [= p and
A7: ( p1 in F & q1 in H ) ;
assume q in D ; :: thesis: p "/\" q in D
then ex r2 being Element of L st
( q = r2 & ex p, q being Element of L st
( p "/\" q [= r2 & p in F & q in H ) ) ;
then consider p2, q2 being Element of L such that
A8: p2 "/\" q2 [= q and
A9: ( p2 in F & q2 in H ) ;
A10: p "/\" (p2 "/\" q2) [= p "/\" q by A8, LATTICES:9;
(p1 "/\" q1) "/\" (p2 "/\" q2) [= p "/\" (p2 "/\" q2) by A6, LATTICES:9;
then A11: (p1 "/\" q1) "/\" (p2 "/\" q2) [= p "/\" q by A10, LATTICES:7;
A12: (p1 "/\" q1) "/\" (p2 "/\" q2) = ((p1 "/\" q1) "/\" p2) "/\" q2 by LATTICES:def 7
.= ((p1 "/\" p2) "/\" q1) "/\" q2 by LATTICES:def 7
.= (p1 "/\" p2) "/\" (q1 "/\" q2) by LATTICES:def 7 ;
( p1 "/\" p2 in F & q1 "/\" q2 in H ) by A7, A9, Th8;
hence p "/\" q in D by A12, A11; :: thesis: verum

end;

then reconsider D = D as Filter of L by A3, Th9;
A13: H c= D

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in H or x in D )
assume x in H ; :: thesis: x in D
then reconsider q = x as Element of H ;
q "/\" p1 [= q by LATTICES:6;
hence x in D by A1; :: thesis: verum

end;

F c= D

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in F or x in D )
assume x in F ; :: thesis: x in D
then reconsider p = x as Element of F ;
p "/\" q1 [= p by LATTICES:6;
hence x in D by A2; :: thesis: verum

end;

then F \/ H c= D by A13, XBOOLE_1:8;
hence <.(F \/ H).) c= { r1 where r1 is Element of L : ex p, q being Element of L st
( p "/\" q [= r1 & p in F & q in H ) } by Def4; :: according to XBOOLE_0:def 10 :: thesis: { r where r is Element of L : ex p, q being Element of L st
( p "/\" q [= r & p in F & q in H ) } c= <.(F \/ H).)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { r where r is Element of L : ex p, q being Element of L st
( p "/\" q [= r & p in F & q in H ) } or x in <.(F \/ H).) )
assume x in { r1 where r1 is Element of L : ex p, q being Element of L st
( p "/\" q [= r1 & p in F & q in H ) } ; :: thesis: x in <.(F \/ H).)
then consider r being Element of L such that
A14: x = r and
A15: ex p, q being Element of L st
( p "/\" q [= r & p in F & q in H ) ;
A16: F \/ H c= <.(F \/ H).) by Def4;
H c= F \/ H by XBOOLE_1:7;
then A17: H c= <.(F \/ H).) by A16;
consider p, q being Element of L such that
A18: p "/\" q [= r and
A19: ( p in F & q in H ) by A15;
F c= F \/ H by XBOOLE_1:7;
then F c= <.(F \/ H).) by A16;
then p "/\" q in <.(F \/ H).) by A19, A17, Th8;
hence x in <.(F \/ H).) by A14, A18, Th9; :: thesis: verum