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} ) & A is open holds
A is upper
let A be Subset of R; :: thesis: ( ( for x being Element of R holds downarrow x = Cl {x} ) & A is open implies A is upper )
assume A1: for x being Element of R holds downarrow x = Cl {x} ; :: thesis: ( not A is open or A is upper )
assume A2: A is open ; :: thesis: A is upper
let x, y be Element of R; :: according to WAYBEL_0:def 20 :: thesis: ( not x in A or not x <= y or y in A )
assume that
A3: x in A and
A4: x <= y ; :: thesis: y in A
x in downarrow y by A4, WAYBEL_0:17;
then x in Cl {y} by A1;
then A meets {y} by A2, A3, PRE_TOPC:24;
then consider z being object such that
A5: z in A /\ {y} by XBOOLE_0:4;
A6: z in A by A5, XBOOLE_0:def 4;
z in {y} by A5, XBOOLE_0:def 4;
hence y in A by A6, TARSKI:def 1; :: thesis: verum