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 object ; :: 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 ;
A2: x >= Top L by A1, WAYBEL_0:18;
x <= Top L by YELLOW_0:45;
then x = Top L by A2, ORDERS_2:2;
hence x in {(Top L)} by TARSKI:def 1; :: thesis: verum

end;

let x be object ; :: 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 A3: x = Top L by TARSKI:def 1;
Top L <= Top L ;
hence x in uparrow (Top L) by A3, WAYBEL_0:18; :: thesis: verum