let L be Lattice; :: thesis: for I, J being Ideal of L holds (.(I \/ J).> = { r where r is Element of L : ex p, q being Element of L st
( r [= p "\/" q & p in I & q in J ) }
let I, J be Ideal of L; :: thesis: (.(I \/ J).> = { r where r is Element of L : ex p, q being Element of L st
( r [= p "\/" q & p in I & q in J ) }
A1: J .: = J ;
( (.(I \/ J).> = <.((I \/ J) .:).) & I .: = I ) by Th36;
then A2: (.(I \/ J).> = { r9 where r9 is Element of (L .:) : ex p9, q9 being Element of (L .:) st
( p9 "/\" q9 [= r9 & p9 in I & q9 in J ) } by A1, FILTER_0:35;
thus (.(I \/ J).> c= { r where r is Element of L : ex p, q being Element of L st
( r [= p "\/" q & p in I & q in J ) } :: according to XBOOLE_0:def 10 :: thesis: { r where r is Element of L : ex p, q being Element of L st
( r [= p "\/" q & p in I & q in J ) } c= (.(I \/ J).>

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (.(I \/ J).> or x in { r where r is Element of L : ex p, q being Element of L st
( r [= p "\/" q & p in I & q in J ) } )
assume x in (.(I \/ J).> ; :: thesis: x in { r where r is Element of L : ex p, q being Element of L st
( r [= p "\/" q & p in I & q in J ) }
then consider r9 being Element of (L .:) such that
A3: x = r9 and
A4: ex p9, q9 being Element of (L .:) st
( p9 "/\" q9 [= r9 & p9 in I & q9 in J ) by A2;
consider p9, q9 being Element of (L .:) such that
A5: p9 "/\" q9 [= r9 and
A6: ( p9 in I & q9 in J ) by A4;
A7: p9 "/\" q9 = (.: p9) "\/" (.: q9) ;
.: r9 [= .: (p9 "/\" q9) by A5, LATTICE2:39;
hence x in { r where r is Element of L : ex p, q being Element of L st
( r [= p "\/" q & p in I & q in J ) } by A3, A6, A7; :: thesis: verum

end;

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
( r [= p "\/" q & p in I & q in J ) } or x in (.(I \/ J).> )
assume x in { r where r is Element of L : ex p, q being Element of L st
( r [= p "\/" q & p in I & q in J ) } ; :: thesis: x in (.(I \/ J).>
then consider r being Element of L such that
A8: x = r and
A9: ex p, q being Element of L st
( r [= p "\/" q & p in I & q in J ) ;
consider p, q being Element of L such that
A10: r [= p "\/" q and
A11: ( p in I & q in J ) by A9;
A12: p "\/" q = (p .:) "/\" (q .:) ;
(p "\/" q) .: [= r .: by A10, LATTICE2:38;
hence x in (.(I \/ J).> by A2, A8, A11, A12; :: thesis: verum