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;
A3: now :: thesis: for a, b being Element of S st a in X & b <= a holds
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;
(waybelow x) /\ S1 is join-closed by Th33;
hence (waybelow x) /\ the carrier of S is Ideal of S by A3, WAYBEL10:23, WAYBEL_0:def 19; :: thesis: verum