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;

now

let x be set ; :: thesis: ( ( x in uparrow (Bottom L) implies x in the carrier of L ) & ( x in the carrier of L implies x in uparrow (Bottom L) ) )
thus ( x in uparrow (Bottom L) implies x in the carrier of L ) ; :: thesis: ( x in the carrier of L implies x in uparrow (Bottom L) )
assume x in the carrier of L ; :: thesis: x in uparrow (Bottom L)
then reconsider x' = x as Element of L ;
Bottom L <= x' by YELLOW_0:44;
hence x in uparrow (Bottom L) by WAYBEL_0:18; :: thesis: verum

end;

hence uparrow (Bottom L) = the carrier of L by TARSKI:2; :: thesis: verum