let T be up-complete lower TopLattice; for A being Subset of T st A is open holds
A is property(S)
defpred S1[ Subset of T] means $1 is property(S) ;
A1:
ex K being prebasis of T st
for A being Subset of T st A in K holds
S1[A]
proof
reconsider K =
{ ((uparrow x) `) where x is Element of T : verum } as
prebasis of
T by Def1;
take
K
;
for A being Subset of T st A in K holds
S1[A]
let A be
Subset of
T;
( A in K implies S1[A] )
assume
A in K
;
S1[A]
then consider x being
Element of
T such that A2:
A = (uparrow x) `
;
let D be non
empty directed Subset of
T;
WAYBEL11:def 3 ( not "\/" (D,T) in A or ex b1 being Element of the carrier of T st
( b1 in D & ( for b2 being Element of the carrier of T holds
( not b2 in D or not b1 <= b2 or b2 in A ) ) ) )
assume A3:
sup D in A
;
ex b1 being Element of the carrier of T st
( b1 in D & ( for b2 being Element of the carrier of T holds
( not b2 in D or not b1 <= b2 or b2 in A ) ) )
set y = the
Element of
D;
reconsider y = the
Element of
D as
Element of
T ;
take
y
;
( y in D & ( for b1 being Element of the carrier of T holds
( not b1 in D or not y <= b1 or b1 in A ) ) )
thus
y in D
;
for b1 being Element of the carrier of T holds
( not b1 in D or not y <= b1 or b1 in A )
let z be
Element of
T;
( not z in D or not y <= z or z in A )
assume that A4:
z in D
and
z >= y
and A5:
not
z in A
;
contradiction
A6:
z >= x
by A5, A2, YELLOW_9:1;
not
x <= sup D
by A3, A2, YELLOW_9:1;
then A7:
not
z <= sup D
by A6, ORDERS_2:3;
A8:
ex_sup_of D,
T
by WAYBEL_0:75;
A9:
ex_sup_of {z},
T
by YELLOW_0:38;
{z} c= D
by A4, ZFMISC_1:31;
then
sup {z} <= sup D
by A8, A9, YELLOW_0:34;
hence
contradiction
by A7, YELLOW_0:39;
verum
end;
A10:
for A1, A2 being Subset of T st S1[A1] & S1[A2] holds
S1[A1 /\ A2]
by Lm3;
A11:
S1[ [#] T]
by Lm4;
A12:
for F being Subset-Family of T st ( for A being Subset of T st A in F holds
S1[A] ) holds
S1[ union F]
by Lm2;
thus
for A being Subset of T st A is open holds
S1[A]
from WAYBEL19:sch 1(A1, A12, A10, A11); verum