let L be lower-bounded continuous sup-Semilattice; :: thesis: for B being with_bottom CLbasis of L holds rng (supMap ()) = the carrier of L
let B be with_bottom CLbasis of L; :: thesis: rng (supMap ()) = the carrier of L
A1: Bottom L in B by Def8;
thus rng (supMap ()) = the carrier of L :: thesis: verum
proof
thus rng (supMap ()) c= the carrier of L ; :: according to XBOOLE_0:def 10 :: thesis: the carrier of L c= rng (supMap ())
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of L or x in rng (supMap ()) )
assume x in the carrier of L ; :: thesis: x in rng (supMap ())
then reconsider x1 = x as Element of L ;
set z = (waybelow x1) /\ B;
(waybelow x1) /\ B is Subset of B by XBOOLE_1:17;
then reconsider z = (waybelow x1) /\ B as Subset of () by YELLOW_0:def 15;
A2: now :: thesis: for a, b being Element of () st a in z & b <= a holds
b in z
let a, b be Element of (); :: thesis: ( a in z & b <= a implies b in z )
reconsider a1 = a, b1 = b as Element of L by YELLOW_0:58;
assume that
A3: a in z and
A4: b <= a ; :: thesis: b in z
a in waybelow x1 by ;
then A5: a1 << x1 by WAYBEL_3:7;
b1 <= a1 by ;
then b1 << x1 by ;
then A6: b in waybelow x1 by WAYBEL_3:7;
b in the carrier of () ;
then b in B by YELLOW_0:def 15;
hence b in z by ; :: thesis: verum
end;
Bottom L << x1 by WAYBEL_3:4;
then A7: Bottom L in waybelow x1 by WAYBEL_3:7;
(waybelow x1) /\ B is join-closed by Th33;
then reconsider z = z as Ideal of () by ;
z in { X where X is Ideal of () : verum } ;
then z in Ids () by WAYBEL_0:def 23;
then A8: z in dom (supMap ()) by Th51;
x = "\/" (z,L) by Def7
.= (supMap ()) . z by Def10 ;
hence x in rng (supMap ()) by ; :: thesis: verum
end;