let L be distributive Lattice; :: thesis: for I being Ideal of L holds I = meet { P where P is Ideal of L : ( P is prime & I c= P ) }
let I be Ideal of L; :: thesis: I = meet { P where P is Ideal of L : ( P is prime & I c= P ) }
X1: [#] L is prime

proof

set II = [#] L;
for p, q being Element of L holds
( p "/\" q in [#] L iff ( p in [#] L or q in [#] L ) ) ;
hence [#] L is prime by FILTER_2:def 10; :: thesis: verum

end;

set P = [#] L;
set X = { P where P is Ideal of L : ( P is prime & I c= P ) } ;
set I1 = meet { P where P is Ideal of L : ( P is prime & I c= P ) } ;
k1: [#] L in { P where P is Ideal of L : ( P is prime & I c= P ) } by X1;
set x = the Element of { P where P is Ideal of L : ( P is prime & I c= P ) } ;
meet { P where P is Ideal of L : ( P is prime & I c= P ) } c= the carrier of L by k1, SETFAM_1:def 1;
then reconsider I2 = meet { P where P is Ideal of L : ( P is prime & I c= P ) } as Subset of L ;
assume meet { P where P is Ideal of L : ( P is prime & I c= P ) } <> I ; :: thesis: contradiction

per cases then ( not meet { P where P is Ideal of L : ( P is prime & I c= P ) } c= I or not I c= meet { P where P is Ideal of L : ( P is prime & I c= P ) } ) ;

suppose not meet { P where P is Ideal of L : ( P is prime & I c= P ) } c= I ; :: thesis: contradiction

then consider a being object such that
A1: ( a in meet { P where P is Ideal of L : ( P is prime & I c= P ) } & not a in I ) ;
a in I2 by A1;
then reconsider a = a as Element of L ;
consider P being Ideal of L such that
A2: ( P is prime & I c= P & not a in P ) by Cor16, A1;
P in { P where P is Ideal of L : ( P is prime & I c= P ) } by A2;
then meet { P where P is Ideal of L : ( P is prime & I c= P ) } c= P by SETFAM_1:3;
hence contradiction by A1, A2; :: thesis: verum

end;

suppose not I c= meet { P where P is Ideal of L : ( P is prime & I c= P ) } ; :: thesis: contradiction

then consider a being object such that
A1: ( a in I & not a in meet { P where P is Ideal of L : ( P is prime & I c= P ) } ) ;
consider Y being set such that
X4: ( Y in { P where P is Ideal of L : ( P is prime & I c= P ) } & not a in Y ) by SETFAM_1:def 1, A1, k1;
consider P1 being Ideal of L such that
X5: ( Y = P1 & P1 is prime & I c= P1 ) by X4;
thus contradiction by A1, X4, X5; :: thesis: verum

end;

end;