let L be RelStr ; :: thesis: for X being Subset of L holds

( X is upper iff uparrow X c= X )

let X be Subset of L; :: thesis: ( X is upper iff uparrow X c= X )

let x, y be Element of L; :: according to WAYBEL_0:def 20 :: thesis: ( x in X & x <= y implies y in X )

assume that

A4: x in X and

A5: y >= x ; :: thesis: y in X

y in uparrow X by A4, A5, Def16;

hence y in X by A3; :: thesis: verum

( X is upper iff uparrow X c= X )

let X be Subset of L; :: thesis: ( X is upper iff uparrow X c= X )

hereby :: thesis: ( uparrow X c= X implies X is upper )

assume A3:
uparrow X c= X
; :: thesis: X is upper assume A1:
X is upper
; :: thesis: uparrow X c= X

thus uparrow X c= X :: thesis: verum

end;thus uparrow X c= X :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in uparrow X or x in X )

assume A2: x in uparrow X ; :: thesis: x in X

then reconsider x9 = x as Element of L ;

ex y being Element of L st

( x9 >= y & y in X ) by A2, Def16;

hence x in X by A1; :: thesis: verum

end;assume A2: x in uparrow X ; :: thesis: x in X

then reconsider x9 = x as Element of L ;

ex y being Element of L st

( x9 >= y & y in X ) by A2, Def16;

hence x in X by A1; :: thesis: verum

let x, y be Element of L; :: according to WAYBEL_0:def 20 :: thesis: ( x in X & x <= y implies y in X )

assume that

A4: x in X and

A5: y >= x ; :: thesis: y in X

y in uparrow X by A4, A5, Def16;

hence y in X by A3; :: thesis: verum