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 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;
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 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