let T be non empty reflexive transitive TopRelStr ; :: thesis: ( the topology of T = { S where S is Subset of T : S is property(S) } implies T is TopSpace-like )
assume A1:
the topology of T = { S where S is Subset of T : S is property(S) }
; :: thesis: T is TopSpace-like
[#] T is property(S)
by Lm2;
hence
the carrier of T in the topology of T
by A1; :: according to PRE_TOPC:def 1 :: thesis: ( ( for b1 being Element of bool (bool the carrier of T) holds
( not b1 c= the topology of T or union b1 in the topology of T ) ) & ( for b1, b2 being Element of bool the carrier of T holds
( not b1 in the topology of T or not b2 in the topology of T or b1 /\ b2 in the topology of T ) ) )
let a, b be Subset of T; :: thesis: ( not a in the topology of T or not b in the topology of T or a /\ b in the topology of T )
assume
a in the topology of T
; :: thesis: ( not b in the topology of T or a /\ b in the topology of T )
then consider A being Subset of T such that
A9:
a = A
and
A10:
A is property(S)
by A1;
assume
b in the topology of T
; :: thesis: a /\ b in the topology of T
then consider B being Subset of T such that
A11:
b = B
and
A12:
B is property(S)
by A1;
A /\ B is property(S)
proof
let D be non
empty directed Subset of
T;
:: according to WAYBEL11:def 3 :: thesis: ( sup D in A /\ B implies ex y being Element of T st
( y in D & ( for x being Element of T st x in D & x >= y holds
x in A /\ B ) ) )
assume A13:
sup D in A /\ B
;
:: thesis: ex y being Element of T st
( y in D & ( for x being Element of T st x in D & x >= y holds
x in A /\ B ) )
then
sup D in A
by XBOOLE_0:def 4;
then consider x being
Element of
T such that A14:
x in D
and A15:
for
z being
Element of
T st
z in D &
z >= x holds
z in A
by A10, Def3;
sup D in B
by A13, XBOOLE_0:def 4;
then consider y being
Element of
T such that A16:
y in D
and A17:
for
z being
Element of
T st
z in D &
z >= y holds
z in B
by A12, Def3;
consider z being
Element of
T such that A18:
z in D
and A19:
x <= z
and A20:
y <= z
by A14, A16, WAYBEL_0:def 1;
take
z
;
:: thesis: ( z in D & ( for x being Element of T st x in D & x >= z holds
x in A /\ B ) )
thus
z in D
by A18;
:: thesis: for x being Element of T st x in D & x >= z holds
x in A /\ B
let u be
Element of
T;
:: thesis: ( u in D & u >= z implies u in A /\ B )
assume A21:
u in D
;
:: thesis: ( not u >= z or u in A /\ B )
assume A22:
u >= z
;
:: thesis: u in A /\ B
then
u >= x
by A19, YELLOW_0:def 2;
then A23:
u in A
by A15, A21;
u >= y
by A20, A22, YELLOW_0:def 2;
then
u in B
by A17, A21;
hence
u in A /\ B
by A23, XBOOLE_0:def 4;
:: thesis: verum
end;
hence
a /\ b in the topology of T
by A1, A9, A11; :: thesis: verum