let T be up-complete lower TopLattice; :: thesis: 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
;
:: thesis: for A being Subset of T st A in K holds
S1[A]
let A be
Subset of
T;
:: thesis: ( A in K implies S1[A] )
assume
A in K
;
:: thesis: S1[A]
then consider x being
Element of
T such that A2:
A = (uparrow x) `
;
let D be non
empty directed Subset of
T;
:: according to WAYBEL11:def 3 :: thesis: ( 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
sup D in A
;
:: thesis: 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 ) ) )
then A3:
not
x <= sup D
by A2, YELLOW_9:1;
consider y being
Element of
D;
reconsider y =
y as
Element of
T ;
take
y
;
:: thesis: ( 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
;
:: thesis: 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;
:: thesis: ( not z in D or not y <= z or z in A )
A4:
(
ex_sup_of D,
T &
ex_sup_of {z},
T )
by WAYBEL_0:75, YELLOW_0:38;
assume
(
z in D &
z >= y & not
z in A )
;
:: thesis: contradiction
then
(
{z} c= D &
z >= x )
by A2, YELLOW_9:1, ZFMISC_1:37;
then
(
sup {z} <= sup D & not
z <= sup D )
by A3, A4, ORDERS_2:26, YELLOW_0:34;
hence
contradiction
by YELLOW_0:39;
:: thesis: verum
end;
A5:
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;
A6:
for A1, A2 being Subset of T st S1[A1] & S1[A2] holds
S1[A1 /\ A2]
by Lm3;
A7:
S1[ [#] T]
by Lm4;
thus
for A being Subset of T st A is open holds
S1[A]
from WAYBEL19:sch 1(A1, A5, A6, A7); :: thesis: verum