let T be non empty transitive lower TopRelStr ; for A being Subset of T st A is open holds
A is lower
reconsider BB = { ((uparrow x) `) where x is Element of T : verum } as prebasis of T by Def1;
let A be Subset of T; ( A is open implies A is lower )
assume A1:
A in the topology of T
; PRE_TOPC:def 2 A is lower
let x, y be Element of T; WAYBEL_0:def 19 ( not x in A or not y <= x or y in A )
consider F being Basis of T such that
A2:
F c= FinMeetCl BB
by CANTOR_1:def 4;
the topology of T c= UniCl F
by CANTOR_1:def 2;
then consider Y being Subset-Family of T such that
A3:
Y c= F
and
A4:
A = union Y
by A1, CANTOR_1:def 1;
assume
x in A
; ( not y <= x or y in A )
then consider Z being set such that
A5:
x in Z
and
A6:
Z in Y
by A4, TARSKI:def 4;
Z in F
by A3, A6;
then consider X being Subset-Family of T such that
A7:
X c= BB
and
X is finite
and
A8:
Z = Intersect X
by A2, CANTOR_1:def 3;
assume A9:
x >= y
; y in A
then
y in Z
by A8, SETFAM_1:43;
hence
y in A
by A4, A6, TARSKI:def 4; verum