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 )

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

assume that

A4: x in X and

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

y in downarrow X by A4, A5, Def15;

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

( 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 A3:
downarrow X c= X
; :: thesis: X is lower assume A1:
X is lower
; :: thesis: downarrow X c= X

thus downarrow X c= X :: thesis: verum

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

proof

let x be object ; :: 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 x9 = x as Element of L ;

ex y being Element of L st

( x9 <= y & y in X ) by A2, Def15;

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

end;assume A2: x in downarrow 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, Def15;

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

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

assume that

A4: x in X and

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

y in downarrow X by A4, A5, Def15;

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