let L be non empty reflexive transitive RelStr ; :: thesis: for x, y being Element of L st x << y holds
for I being Ideal of L st y <= sup I holds
x in I
let x, y be Element of L; :: thesis: ( x << y implies for I being Ideal of L st y <= sup I holds
x in I )
assume A1: x << y ; :: 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 y <= sup I ; :: thesis: x in I
then ex d being Element of L st
( d in I & x <= d ) by A1;
hence x in I by WAYBEL_0:def 19; :: thesis: verum