let R be non empty TopRelStr ; :: thesis: for A being Subset of R st ( for x being Element of R holds downarrow x = Cl {x} ) holds
for A being Subset of R st A is closed holds
A is lower
let A be Subset of R; :: thesis: ( ( for x being Element of R holds downarrow x = Cl {x} ) implies for A being Subset of R st A is closed holds
A is lower )
assume A1: for x being Element of R holds downarrow x = Cl {x} ; :: thesis: for A being Subset of R st A is closed holds
A is lower
let A be Subset of R; :: thesis: ( A is closed implies A is lower )
assume A2: A is closed ; :: thesis: A is lower
let x, y be Element of R; :: according to WAYBEL_0:def 19 :: thesis: ( not x in A or not y <= x or y in A )
assume that
A3: x in A and
A4: y <= x ; :: thesis: y in A
y in downarrow x by A4, WAYBEL_0:17;
then A5: y in Cl {x} by A1;
{x} c= A by A3, TARSKI:def 1;
hence y in A by A2, A5, PRE_TOPC:15; :: thesis: verum