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 ) }
( (.(I \/ J).> = <.((I \/ J) .: ).) & (I \/ J) .: = I \/ J & I .: = I & J .: = J ) by Th37;
then A1: (.(I \/ J).> = { r' where r' is Element of (L .: ) : ex p', q' being Element of (L .: ) st
( p' "/\" q' [= r' & p' in I & q' in J ) } by FILTER_0:48;
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 set ; :: 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 r' being Element of (L .: ) such that
A2: ( x = r' & ex p', q' being Element of (L .: ) st
( p' "/\" q' [= r' & p' in I & q' in J ) ) by A1;
consider p', q' being Element of (L .: ) such that
A3: ( p' "/\" q' [= r' & p' in I & q' in J ) by A2;
( .: r' [= .: (p' "/\" q') & .: (p' "/\" q') = p' "/\" q' & p' "/\" q' = (.: p') "\/" (.: q') & .: p' = p' & .: q' = q' & .: r' = r' ) by A3, LATTICE2:54;
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 A2, A3; :: thesis: verum

end;

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
( 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
A4: ( x = r & 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
A5: ( r [= p "\/" q & p in I & q in J ) by A4;
( (p "\/" q) .: [= r .: & (p "\/" q) .: = p "\/" q & p "\/" q = (p .: ) "/\" (q .: ) & p .: = p & q .: = q & r .: = r ) by A5, LATTICE2:53;
hence x in (.(I \/ J).> by A1, A4, A5; :: thesis: verum