let L be Lattice; :: thesis: for I being Ideal of L holds (.I.> = I
let I be Ideal of L; :: thesis: (.I.> = I
( (.I.> c= I & I c= (.I.> ) by Def11;
hence (.I.> = I by XBOOLE_0:def 10; :: thesis: verum