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;
for x being object holds
( x in downarrow (Top L) iff x in the carrier of L ) by WAYBEL_0:17, YELLOW_0:45;
hence downarrow (Top L) = the carrier of L by TARSKI:2; :: thesis: verum