let L be RelStr ; :: thesis: for X being Subset of L holds
( X is lower iff downarrow X c= X )
let X be Subset of L; :: thesis: ( X is lower iff downarrow X c= X )

hereby :: thesis: ( downarrow X c= X implies X is lower )

assume A1: X is lower ; :: thesis: downarrow X c= X
thus downarrow X c= X :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in downarrow X or x in X )
assume A2: x in downarrow X ; :: thesis: x in X
then reconsider x' = x as Element of L ;
ex y being Element of L st
( x' <= y & y in X ) by A2, Def15;
hence x in X by A1, Def19; :: thesis: verum

end;

end;

assume A3: downarrow X c= X ; :: thesis: X is lower
let x, y be Element of L; :: according to WAYBEL_0:def 19 :: thesis: ( x in X & y <= x implies y in X )
assume ( x in X & y <= x ) ; :: thesis: y in X
then y in downarrow X by Def15;
hence y in X by A3; :: thesis: verum