let L be distributive complete LATTICE; :: thesis: for x, y being Element of L holds
( x << y iff for P being prime Ideal of L st y <= sup P holds
x in P )
let x, y be Element of L; :: thesis: ( x << y iff for P being prime Ideal of L st y <= sup P holds
x in P )
thus ( x << y implies for P being prime Ideal of L st y <= sup P holds
x in P ) by WAYBEL_3:20; :: thesis: ( ( for P being prime Ideal of L st y <= sup P holds
x in P ) implies x << y )
assume A1: for P being prime Ideal of L st y <= sup P holds
x in P ; :: thesis: x << y

now

let I be Ideal of L; :: thesis: ( y <= sup I implies x in I )
assume A2: ( y <= sup I & not x in I ) ; :: thesis: contradiction
then consider P being Ideal of L such that
A3: ( P is prime & I c= P & not x in P ) by Th28;
sup I <= sup P by A3, Th3;
hence contradiction by A1, A2, A3, ORDERS_2:26; :: thesis: verum

end;

hence x << y by WAYBEL_3:21; :: thesis: verum