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 )

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

assume A1: X is upper ; :: thesis: uparrow X c= X
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;

end;

assume A3: uparrow X c= X ; :: thesis: X is upper
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