let L be Lattice; :: thesis: for F, H 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 F, H 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 Th11;
consider q1 being Element of L such that
A2: q1 in H by Th11;
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 set ; :: 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 & 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 A4: 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 ) ) ;
assume q in D ; :: thesis: p "/\" q in D
then A5: 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 ) ) ;
consider p1, q1 being Element of L such that
A6: ( p1 "/\" q1 [= p & p1 in F & q1 in H ) by A4;
consider p2, q2 being Element of L such that
A7: ( p2 "/\" q2 [= q & p2 in F & q2 in H ) by A5;
A8: (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 "/\" q1) "/\" (p2 "/\" q2) [= p "/\" (p2 "/\" q2) & p "/\" (p2 "/\" q2) [= p "/\" q ) by A6, A7, LATTICES:27;
then ( p1 "/\" p2 in F & q1 "/\" q2 in H & (p1 "/\" q1) "/\" (p2 "/\" q2) [= p "/\" q ) by A6, A7, Def1, LATTICES:25;
hence p "/\" q in D by A8; :: thesis: verum

end;

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
A9: ( p1 "/\" q1 [= p & p1 in F & q1 in H ) ;
assume p [= q ; :: thesis: q in D
then p1 "/\" q1 [= q by A9, LATTICES:25;
hence q in D by A9; :: thesis: verum

end;

then reconsider D = D as Filter of L by A3, Th9;
A10: F c= D

proof

let x be set ; :: 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:23;
hence x in D by A2; :: thesis: verum

end;

H c= D

proof

let x be set ; :: 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 ;
( p1 "/\" q = q "/\" p1 & q "/\" p1 [= q ) by LATTICES:23;
hence x in D by A1; :: thesis: verum

end;

then F \/ H c= D by A10, 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 Def5; :: 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 set ; :: 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
A11: ( x = r & ex p, q being Element of L st
( p "/\" q [= r & p in F & q in H ) ) ;
consider p, q being Element of L such that
A12: ( p "/\" q [= r & p in F & q in H ) by A11;
( F c= F \/ H & H c= F \/ H & F \/ H c= <.(F \/ H).) ) by Def5, XBOOLE_1:7;
then ( F c= <.(F \/ H).) & H c= <.(F \/ H).) ) by XBOOLE_1:1;
then p "/\" q in <.(F \/ H).) by A12, Def1;
hence x in <.(F \/ H).) by A11, A12, Th9; :: thesis: verum