let T be non empty transitive lower TopRelStr ; :: thesis: 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; :: thesis: ( A is open implies A is lower )
assume A1: A in the topology of T ; :: according to PRE_TOPC:def 2 :: thesis: A is lower
let x, y be Element of T; :: according to WAYBEL_0:def 19 :: thesis: ( 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 ; :: thesis: ( 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 ; :: thesis: y in A

now :: thesis: for Q being set st Q in X holds
y in Q

let Q be set ; :: thesis: ( Q in X implies y in Q )
assume A10: Q in X ; :: thesis: y in Q
then Q in BB by A7;
then consider z being Element of T such that
A11: Q = (uparrow z) ` ;
uparrow z misses Q by A11, XBOOLE_1:79;
then A12: (uparrow z) /\ Q = {} T ;
x in Q by A5, A8, A10, SETFAM_1:43;
then not x in uparrow z by A12, XBOOLE_0:def 4;
then not x >= z by WAYBEL_0:18;
then not y >= z by A9, ORDERS_2:3;
then not y in uparrow z by WAYBEL_0:18;
hence y in Q by A11, XBOOLE_0:def 5; :: thesis: verum

end;

then y in Z by A8, SETFAM_1:43;
hence y in A by A4, A6, TARSKI:def 4; :: thesis: verum