let L be non empty antisymmetric upper-bounded RelStr ; :: thesis: for X being non empty Subset of L holds Top L in uparrow X

let X be non empty Subset of L; :: thesis: Top L in uparrow X

consider y being object such that

A1: y in X by XBOOLE_0:def 1;

reconsider y = y as Element of X by A1;

( uparrow X = { x where x is Element of L : ex y being Element of L st

( x >= y & y in X ) } & Top L >= y ) by WAYBEL_0:15, YELLOW_0:45;

hence Top L in uparrow X ; :: thesis: verum

let X be non empty Subset of L; :: thesis: Top L in uparrow X

consider y being object such that

A1: y in X by XBOOLE_0:def 1;

reconsider y = y as Element of X by A1;

( uparrow X = { x where x is Element of L : ex y being Element of L st

( x >= y & y in X ) } & Top L >= y ) by WAYBEL_0:15, YELLOW_0:45;

hence Top L in uparrow X ; :: thesis: verum