let T be non empty transitive lower TopRelStr ; :: thesis: for A being Subset of T st A is closed holds
A is upper
let A be Subset of T; :: thesis: ( A is closed implies A is upper )
assume ([#] T) \ A in the topology of T ; :: according to PRE_TOPC:def 5,PRE_TOPC:def 6 :: thesis: A is upper
then A ` is open by PRE_TOPC:def 5;
then A1: A ` is lower by Th5;
let x, y be Element of T; :: according to WAYBEL_0:def 20 :: thesis: ( not x in A or not x <= y or y in A )
assume A2: ( x in A & x <= y & not y in A ) ; :: thesis: contradiction
then ( not x in A ` & y in A ` ) by XBOOLE_0:def 5;
hence contradiction by A1, A2, WAYBEL_0:def 19; :: thesis: verum