let L be lower-bounded sup-Semilattice; :: thesis: for S being non empty full SubRelStr of L st Bottom L in the carrier of S & the carrier of S is join-closed Subset of L holds

for x being Element of L holds (waybelow x) /\ the carrier of S is Ideal of S

let S be non empty full SubRelStr of L; :: thesis: ( Bottom L in the carrier of S & the carrier of S is join-closed Subset of L implies for x being Element of L holds (waybelow x) /\ the carrier of S is Ideal of S )

assume that

A1: Bottom L in the carrier of S and

A2: the carrier of S is join-closed Subset of L ; :: thesis: for x being Element of L holds (waybelow x) /\ the carrier of S is Ideal of S

let x be Element of L; :: thesis: (waybelow x) /\ the carrier of S is Ideal of S

Bottom L << x by WAYBEL_3:4;

then Bottom L in waybelow x by WAYBEL_3:7;

then reconsider X = (waybelow x) /\ the carrier of S as non empty Subset of S by A1, XBOOLE_0:def 4, XBOOLE_1:17;

reconsider S1 = the carrier of S as join-closed Subset of L by A2;

hence (waybelow x) /\ the carrier of S is Ideal of S by A3, WAYBEL10:23, WAYBEL_0:def 19; :: thesis: verum

for x being Element of L holds (waybelow x) /\ the carrier of S is Ideal of S

let S be non empty full SubRelStr of L; :: thesis: ( Bottom L in the carrier of S & the carrier of S is join-closed Subset of L implies for x being Element of L holds (waybelow x) /\ the carrier of S is Ideal of S )

assume that

A1: Bottom L in the carrier of S and

A2: the carrier of S is join-closed Subset of L ; :: thesis: for x being Element of L holds (waybelow x) /\ the carrier of S is Ideal of S

let x be Element of L; :: thesis: (waybelow x) /\ the carrier of S is Ideal of S

Bottom L << x by WAYBEL_3:4;

then Bottom L in waybelow x by WAYBEL_3:7;

then reconsider X = (waybelow x) /\ the carrier of S as non empty Subset of S by A1, XBOOLE_0:def 4, XBOOLE_1:17;

reconsider S1 = the carrier of S as join-closed Subset of L by A2;

A3: now :: thesis: for a, b being Element of S st a in X & b <= a holds

b in X

(waybelow x) /\ S1 is join-closed
by Th33;b in X

let a, b be Element of S; :: thesis: ( a in X & b <= a implies b in X )

reconsider a1 = a, b1 = b as Element of L by YELLOW_0:58;

assume that

A4: a in X and

A5: b <= a ; :: thesis: b in X

a in waybelow x by A4, XBOOLE_0:def 4;

then A6: a1 << x by WAYBEL_3:7;

b1 <= a1 by A5, YELLOW_0:59;

then b1 << x by A6, WAYBEL_3:2;

then b in waybelow x by WAYBEL_3:7;

hence b in X by XBOOLE_0:def 4; :: thesis: verum

end;reconsider a1 = a, b1 = b as Element of L by YELLOW_0:58;

assume that

A4: a in X and

A5: b <= a ; :: thesis: b in X

a in waybelow x by A4, XBOOLE_0:def 4;

then A6: a1 << x by WAYBEL_3:7;

b1 <= a1 by A5, YELLOW_0:59;

then b1 << x by A6, WAYBEL_3:2;

then b in waybelow x by WAYBEL_3:7;

hence b in X by XBOOLE_0:def 4; :: thesis: verum

hence (waybelow x) /\ the carrier of S is Ideal of S by A3, WAYBEL10:23, WAYBEL_0:def 19; :: thesis: verum