let L be Lattice; :: thesis: for I, J being Ideal of L holds (.(I \/ J).> = { r where r is Element of : ex p, q being Element of 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 : ex p, q being Element of st
( r [= p "\/" q & p in I & q in J ) }
A1: J .: = J ;
( (.(I \/ J).> = <.((I \/ J) .: ).) & I .: = I ) by Th37;
then A2: (.(I \/ J).> = { r' where r' is Element of : ex p', q' being Element of st
( p' "/\" q' [= r' & p' in I & q' in J ) } by A1, FILTER_0:48;
thus (.(I \/ J).> c= { r where r is Element of : ex p, q being Element of st
( r [= p "\/" q & p in I & q in J ) } :: according to XBOOLE_0:def 10 :: thesis: { r where r is Element of : ex p, q being Element of 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 : ex p, q being Element of st
( r [= p "\/" q & p in I & q in J ) } )
assume x in (.(I \/ J).> ; :: thesis: x in { r where r is Element of : ex p, q being Element of st
( r [= p "\/" q & p in I & q in J ) }
then consider r' being Element of such that
A3: x = r' and
A4: ex p', q' being Element of st
( p' "/\" q' [= r' & p' in I & q' in J ) by A2;
consider p', q' being Element of such that
A5: p' "/\" q' [= r' and
A6: ( p' in I & q' in J ) by A4;
A7: p' "/\" q' = (.: p') "\/" (.: q') ;
.: r' [= .: (p' "/\" q') by A5, LATTICE2:54;
hence x in { r where r is Element of : ex p, q being Element of st
( r [= p "\/" q & p in I & q in J ) } by A3, A6, A7; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { r where r is Element of : ex p, q being Element of st
( r [= p "\/" q & p in I & q in J ) } or x in (.(I \/ J).> )
assume x in { r where r is Element of : ex p, q being Element of st
( r [= p "\/" q & p in I & q in J ) } ; :: thesis: x in (.(I \/ J).>
then consider r being Element of such that
A8: x = r and
A9: ex p, q being Element of st
( r [= p "\/" q & p in I & q in J ) ;
consider p, q being Element of 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:53;
hence x in (.(I \/ J).> by A2, A8, A11, A12; :: thesis: verum