let L be up-complete Semilattice; :: thesis: ( ( for x being Element of L ex I being Ideal of L st

( x <= sup I & ( for J being Ideal of L st x <= sup J holds

I c= J ) ) ) implies L is continuous )

assume A1: for x being Element of L ex I being Ideal of L st

( x <= sup I & ( for J being Ideal of L st x <= sup J holds

I c= J ) ) ; :: thesis: L is continuous

( x <= sup I & ( for J being Ideal of L st x <= sup J holds

I c= J ) ) ) implies L is continuous )

assume A1: for x being Element of L ex I being Ideal of L st

( x <= sup I & ( for J being Ideal of L st x <= sup J holds

I c= J ) ) ; :: thesis: L is continuous

now :: thesis: for x being Element of L holds

( waybelow x is Ideal of L & x <= sup (waybelow x) & ( for I being Ideal of L st x <= sup I holds

waybelow x c= I ) )

hence
L is continuous
by Lm2; :: thesis: verum( waybelow x is Ideal of L & x <= sup (waybelow x) & ( for I being Ideal of L st x <= sup I holds

waybelow x c= I ) )

let x be Element of L; :: thesis: ( waybelow x is Ideal of L & x <= sup (waybelow x) & ( for I being Ideal of L st x <= sup I holds

waybelow x c= I ) )

consider I being Ideal of L such that

A2: x <= sup I and

A3: for J being Ideal of L st x <= sup J holds

I c= J by A1;

for y being object st y in waybelow x holds

y in I by A2, WAYBEL_3:7, WAYBEL_3:20;

then waybelow x c= I ;

then waybelow x = I by A5, XBOOLE_0:def 10;

hence ( waybelow x is Ideal of L & x <= sup (waybelow x) & ( for I being Ideal of L st x <= sup I holds

waybelow x c= I ) ) by A2, A3; :: thesis: verum

end;waybelow x c= I ) )

consider I being Ideal of L such that

A2: x <= sup I and

A3: for J being Ideal of L st x <= sup J holds

I c= J by A1;

now :: thesis: for y being object st y in I holds

y in waybelow x

then A5:
I c= waybelow x
;y in waybelow x

let y be object ; :: thesis: ( y in I implies y in waybelow x )

assume A4: y in I ; :: thesis: y in waybelow x

then reconsider y9 = y as Element of L ;

for J being Ideal of L st x <= sup J holds

y in J

hence y in waybelow x by WAYBEL_3:7; :: thesis: verum

end;assume A4: y in I ; :: thesis: y in waybelow x

then reconsider y9 = y as Element of L ;

for J being Ideal of L st x <= sup J holds

y in J

proof

then
y9 << x
by WAYBEL_3:21;
let J be Ideal of L; :: thesis: ( x <= sup J implies y in J )

assume x <= sup J ; :: thesis: y in J

then I c= J by A3;

hence y in J by A4; :: thesis: verum

end;assume x <= sup J ; :: thesis: y in J

then I c= J by A3;

hence y in J by A4; :: thesis: verum

hence y in waybelow x by WAYBEL_3:7; :: thesis: verum

for y being object st y in waybelow x holds

y in I by A2, WAYBEL_3:7, WAYBEL_3:20;

then waybelow x c= I ;

then waybelow x = I by A5, XBOOLE_0:def 10;

hence ( waybelow x is Ideal of L & x <= sup (waybelow x) & ( for I being Ideal of L st x <= sup I holds

waybelow x c= I ) ) by A2, A3; :: thesis: verum