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