let X be set ; for A being Subset-Family of X holds TopStruct(# X,(UniCl (FinMeetCl A)) #) is TopSpace-like
let A be Subset-Family of X; TopStruct(# X,(UniCl (FinMeetCl A)) #) is TopSpace-like
per cases
( X = {} or X <> {} )
;
suppose A1:
X = {}
;
TopStruct(# X,(UniCl (FinMeetCl A)) #) is TopSpace-like set T =
TopStruct(#
X,
(UniCl (FinMeetCl A)) #);
( the
carrier of
TopStruct(#
X,
(UniCl (FinMeetCl A)) #)
in FinMeetCl A &
FinMeetCl A c= UniCl (FinMeetCl A) )
by CANTOR_1:1, CANTOR_1:8;
hence
the
carrier of
TopStruct(#
X,
(UniCl (FinMeetCl A)) #)
in the
topology of
TopStruct(#
X,
(UniCl (FinMeetCl A)) #)
;
PRE_TOPC:def 1 ( ( for b1 being Element of K19(K19( the carrier of TopStruct(# X,(UniCl (FinMeetCl A)) #))) holds
( not b1 c= the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) or union b1 in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) ) ) & ( for b1, b2 being Element of K19( the carrier of TopStruct(# X,(UniCl (FinMeetCl A)) #)) holds
( not b1 in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) or not b2 in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) or b1 /\ b2 in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) ) ) )hence
for
a being
Subset-Family of
TopStruct(#
X,
(UniCl (FinMeetCl A)) #) st
a c= the
topology of
TopStruct(#
X,
(UniCl (FinMeetCl A)) #) holds
union a in the
topology of
TopStruct(#
X,
(UniCl (FinMeetCl A)) #)
by A1;
for b1, b2 being Element of K19( the carrier of TopStruct(# X,(UniCl (FinMeetCl A)) #)) holds
( not b1 in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) or not b2 in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) or b1 /\ b2 in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) )thus
for
b1,
b2 being
Element of
K19( the
carrier of
TopStruct(#
X,
(UniCl (FinMeetCl A)) #)) holds
( not
b1 in the
topology of
TopStruct(#
X,
(UniCl (FinMeetCl A)) #) or not
b2 in the
topology of
TopStruct(#
X,
(UniCl (FinMeetCl A)) #) or
b1 /\ b2 in the
topology of
TopStruct(#
X,
(UniCl (FinMeetCl A)) #) )
by A1;
verum end;