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 :: thesis: for I being Ideal of L st y <= sup I holds
x in I

let I be Ideal of L; :: thesis: ( y <= sup I implies x in I )
assume that
A2: y <= sup I and
A3: not x in I ; :: thesis: contradiction
consider P being Ideal of L such that
A4: P is prime and
A5: I c= P and
A6: not x in P by A3, Th24;
sup I <= sup P by A5, Th1;
hence contradiction by A1, A2, A4, A6, ORDERS_2:3; :: thesis: verum

end;

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