let L be non empty antisymmetric lower-bounded RelStr ; :: thesis: uparrow (Bottom L) = the carrier of L
set uL = uparrow (Bottom L);
set cL = the carrier of L;
for x being object holds
( x in uparrow (Bottom L) iff x in the carrier of L ) by WAYBEL_0:18, YELLOW_0:44;
hence uparrow (Bottom L) = the carrier of L by TARSKI:2; :: thesis: verum