let L be non empty RelStr ; :: thesis: for X being Subset of L holds uparrow X = { x where x is Element of L : ex y being Element of L st

( x >= y & y in X ) }

let X be Subset of L; :: thesis: uparrow X = { x where x is Element of L : ex y being Element of L st

( x >= y & y in X ) }

set Y = { x where x is Element of L : ex y being Element of L st

( x >= y & y in X ) } ;

( x >= y & y in X ) } or x in uparrow X )

assume x in { x where x is Element of L : ex y being Element of L st

( x >= y & y in X ) } ; :: thesis: x in uparrow X

then ex a being Element of L st

( a = x & ex y being Element of L st

( a >= y & y in X ) ) ;

hence x in uparrow X by Def16; :: thesis: verum

( x >= y & y in X ) }

let X be Subset of L; :: thesis: uparrow X = { x where x is Element of L : ex y being Element of L st

( x >= y & y in X ) }

set Y = { x where x is Element of L : ex y being Element of L st

( x >= y & y in X ) } ;

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: { x where x is Element of L : ex y being Element of L st

( x >= y & y in X ) } c= uparrow X

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { x where x is Element of L : ex y being Element of L st ( x >= y & y in X ) } c= uparrow X

let x be object ; :: thesis: ( x in uparrow X implies x in { x where x is Element of L : ex y being Element of L st

( x >= y & y in X ) } )

assume A1: x in uparrow X ; :: thesis: x in { x where x is Element of L : ex y being Element of L st

( x >= y & y in X ) }

then reconsider y = x as Element of L ;

ex z being Element of L st

( z <= y & z in X ) by A1, Def16;

hence x in { x where x is Element of L : ex y being Element of L st

( x >= y & y in X ) } ; :: thesis: verum

end;( x >= y & y in X ) } )

assume A1: x in uparrow X ; :: thesis: x in { x where x is Element of L : ex y being Element of L st

( x >= y & y in X ) }

then reconsider y = x as Element of L ;

ex z being Element of L st

( z <= y & z in X ) by A1, Def16;

hence x in { x where x is Element of L : ex y being Element of L st

( x >= y & y in X ) } ; :: thesis: verum

( x >= y & y in X ) } or x in uparrow X )

assume x in { x where x is Element of L : ex y being Element of L st

( x >= y & y in X ) } ; :: thesis: x in uparrow X

then ex a being Element of L st

( a = x & ex y being Element of L st

( a >= y & y in X ) ) ;

hence x in uparrow X by Def16; :: thesis: verum