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 ) ) )
hereby :: thesis: 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 be Subset-Family of T; :: thesis: ( a c= the topology of T implies union a in the topology of T )
assume A2: a c= the topology of T ; :: thesis: union a in the topology of T
union a is property(S)
proof
let D be non empty directed Subset of T; :: according to WAYBEL11:def 3 :: thesis: ( sup D in union a 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 union a ) ) )
assume sup D in union a ; :: 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 union a ) )
then consider x being set such that
A3: sup D in x and
A4: x in a by TARSKI:def 4;
x in the topology of T by A2, A4;
then consider X being Subset of T such that
A5: x = X and
A6: X is property(S) by A1;
consider y being Element of T such that
A7: y in D and
A8: for x being Element of T st x in D & x >= y holds
x in X by A3, A5, A6;
take y ; :: thesis: ( y in D & ( for x being Element of T st x in D & x >= y holds
x in union a ) )
thus y in D by A7; :: thesis: for x being Element of T st x in D & x >= y holds
x in union a
let u be Element of T; :: thesis: ( u in D & u >= y implies u in union a )
assume that
A9: u in D and
A10: u >= y ; :: thesis: u in union a
u in X by A8, A9, A10;
hence u in union a by A4, A5, TARSKI:def 4; :: thesis: verum
end;
hence union a in the topology of T by A1; :: thesis: verum
end;
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
A11: a = A and
A12: 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
A13: b = B and
A14: 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 A15: 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
A16: x in D and
A17: for z being Element of T st z in D & z >= x holds
z in A by A12;
sup D in B by A15, XBOOLE_0:def 4;
then consider y being Element of T such that
A18: y in D and
A19: for z being Element of T st z in D & z >= y holds
z in B by A14;
consider z being Element of T such that
A20: z in D and
A21: x <= z and
A22: y <= z by A16, A18, 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 A20; :: 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 A23: u in D ; :: thesis: ( not u >= z or u in A /\ B )
assume A24: u >= z ; :: thesis: u in A /\ B
then u >= x by A21, YELLOW_0:def 2;
then A25: u in A by A17, A23;
u >= y by A22, A24, YELLOW_0:def 2;
then u in B by A19, A23;
hence u in A /\ B by A25, XBOOLE_0:def 4; :: thesis: verum
end;
hence a /\ b in the topology of T by A1, A11, A13; :: thesis: verum