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

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;

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;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

Bottom L << x1
by WAYBEL_3:4;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;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

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