let L be lower-bounded continuous sup-Semilattice; :: thesis: for B being with_bottom CLbasis of L holds rng (supMap (subrelstr B)) = the carrier of L
let B be with_bottom CLbasis of L; :: thesis: rng (supMap (subrelstr B)) = the carrier of L
A1: Bottom L in B by Def8;
thus rng (supMap (subrelstr B)) = the carrier of L :: thesis: verum
proof
thus rng (supMap (subrelstr B)) c= the carrier of L ; :: according to XBOOLE_0:def 10 :: thesis: the carrier of L c= rng (supMap (subrelstr B))
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of L or x in rng (supMap (subrelstr B)) )
assume x in the carrier of L ; :: thesis: x in rng (supMap (subrelstr B))
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 (subrelstr B) by YELLOW_0:def 15;
A2: now :: thesis: for a, b being Element of (subrelstr B) st a in z & b <= a holds
b in z
let a, b be Element of (subrelstr B); :: 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 A3, XBOOLE_0:def 4;
then A5: a1 << x1 by WAYBEL_3:7;
b1 <= a1 by A4, YELLOW_0:59;
then b1 << x1 by A5, WAYBEL_3:2;
then A6: b in waybelow x1 by WAYBEL_3:7;
b in the carrier of (subrelstr B) ;
then b in B by YELLOW_0:def 15;
hence b in z by A6, XBOOLE_0:def 4; :: 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 (subrelstr B) by A1, A7, A2, WAYBEL10:23, WAYBEL_0:def 19, XBOOLE_0:def 4;
z in { X where X is Ideal of (subrelstr B) : verum } ;
then z in Ids (subrelstr B) by WAYBEL_0:def 23;
then A8: z in dom (supMap (subrelstr B)) by Th51;
x = "\/" (z,L) by Def7
.= (supMap (subrelstr B)) . z by Def10 ;
hence x in rng (supMap (subrelstr B)) by A8, FUNCT_1:def 3; :: thesis: verum
end;