let L be non empty antisymmetric upper-bounded RelStr ; :: thesis: downarrow (Top L) = the carrier of L
set uL = downarrow (Top L);
set cL = the carrier of L;

now

let x be set ; :: thesis: ( ( x in downarrow (Top L) implies x in the carrier of L ) & ( x in the carrier of L implies x in downarrow (Top L) ) )
thus ( x in downarrow (Top L) implies x in the carrier of L ) ; :: thesis: ( x in the carrier of L implies x in downarrow (Top L) )
assume x in the carrier of L ; :: thesis: x in downarrow (Top L)
then reconsider x9 = x as Element of L ;
Top L >= x9 by YELLOW_0:45;
hence x in downarrow (Top L) by WAYBEL_0:17; :: thesis: verum

end;

hence downarrow (Top L) = the carrier of L by TARSKI:1; :: thesis: verum