let L be non empty upper-bounded Poset; :: thesis: uparrow (Top L) = {(Top L)}
thus uparrow (Top L) c= {(Top L)} :: according to XBOOLE_0:def 10 :: thesis: {(Top L)} c= uparrow (Top L)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in uparrow (Top L) or x in {(Top L)} )
assume A1: x in uparrow (Top L) ; :: thesis: x in {(Top L)}
then reconsider x = x as Element of L ;
( x >= Top L & x <= Top L ) by A1, WAYBEL_0:18, YELLOW_0:45;
then x = Top L by ORDERS_2:25;
hence x in {(Top L)} by TARSKI:def 1; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {(Top L)} or x in uparrow (Top L) )
assume x in {(Top L)} ; :: thesis: x in uparrow (Top L)
then ( x = Top L & Top L <= Top L ) by TARSKI:def 1;
hence x in uparrow (Top L) by WAYBEL_0:18; :: thesis: verum