let X be set ; for F being Subset-Family of X st {} in F & ( for A, B being set st A in F & B in F holds
A \/ B in F ) & ( for G being Subset-Family of X st G c= F holds
Intersect G in F ) holds
for T being TopStruct st the carrier of T = X & the topology of T = COMPLEMENT F holds
( T is TopSpace & ( for A being Subset of T holds
( A is closed iff A in F ) ) )
let F be Subset-Family of X; ( {} in F & ( for A, B being set st A in F & B in F holds
A \/ B in F ) & ( for G being Subset-Family of X st G c= F holds
Intersect G in F ) implies for T being TopStruct st the carrier of T = X & the topology of T = COMPLEMENT F holds
( T is TopSpace & ( for A being Subset of T holds
( A is closed iff A in F ) ) ) )
assume A1:
{} in F
; ( ex A, B being set st
( A in F & B in F & not A \/ B in F ) or ex G being Subset-Family of X st
( G c= F & not Intersect G in F ) or for T being TopStruct st the carrier of T = X & the topology of T = COMPLEMENT F holds
( T is TopSpace & ( for A being Subset of T holds
( A is closed iff A in F ) ) ) )
set O = COMPLEMENT F;
assume A2:
for A, B being set st A in F & B in F holds
A \/ B in F
; ( ex G being Subset-Family of X st
( G c= F & not Intersect G in F ) or for T being TopStruct st the carrier of T = X & the topology of T = COMPLEMENT F holds
( T is TopSpace & ( for A being Subset of T holds
( A is closed iff A in F ) ) ) )
assume A3:
for G being Subset-Family of X st G c= F holds
Intersect G in F
; for T being TopStruct st the carrier of T = X & the topology of T = COMPLEMENT F holds
( T is TopSpace & ( for A being Subset of T holds
( A is closed iff A in F ) ) )
let T be TopStruct ; ( the carrier of T = X & the topology of T = COMPLEMENT F implies ( T is TopSpace & ( for A being Subset of T holds
( A is closed iff A in F ) ) ) )
assume that
A4:
the carrier of T = X
and
A5:
the topology of T = COMPLEMENT F
; ( T is TopSpace & ( for A being Subset of T holds
( A is closed iff A in F ) ) )
T is TopSpace-like
proof
({} T) ` in COMPLEMENT F
by A1, A4, SETFAM_1:35;
hence
the
carrier of
T in the
topology of
T
by A5;
PRE_TOPC:def 1 ( ( 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;
( not a in the topology of T or not b in the topology of T or a /\ b in the topology of T )
assume that A6:
a in the
topology of
T
and A7:
b in the
topology of
T
;
a /\ b in the topology of T
A8:
b ` in F
by A7, A4, A5, SETFAM_1:def 7;
a ` in F
by A6, A4, A5, SETFAM_1:def 7;
then
(a `) \/ (b `) in F
by A8, A2;
then
(a /\ b) ` in F
by XBOOLE_1:54;
hence
a /\ b in the
topology of
T
by A4, A5, SETFAM_1:def 7;
verum
end;
hence
T is TopSpace
; for A being Subset of T holds
( A is closed iff A in F )
let A be Subset of T; ( A is closed iff A in F )
( A is closed iff A ` is open )
;
then
( A is closed iff A ` in COMPLEMENT F )
by A5;
hence
( A is closed iff A in F )
by A4, SETFAM_1:35; verum