let X be set ; :: thesis: for A being Subset-Family of X holds TopStruct(# X,(UniCl (FinMeetCl A)) #) is TopSpace-like
let A be Subset-Family of X; :: thesis: TopStruct(# X,(UniCl (FinMeetCl A)) #) is TopSpace-like
per cases
( X = {} or X <> {} )
;
suppose A1:
X = {}
;
:: thesis: TopStruct(# X,(UniCl (FinMeetCl A)) #) is TopSpace-likeset T =
TopStruct(#
X,
(UniCl (FinMeetCl A)) #);
A2:
the
carrier of
TopStruct(#
X,
(UniCl (FinMeetCl A)) #)
in FinMeetCl A
by CANTOR_1:8;
FinMeetCl A c= UniCl (FinMeetCl A)
by CANTOR_1:1;
hence
the
carrier of
TopStruct(#
X,
(UniCl (FinMeetCl A)) #)
in the
topology of
TopStruct(#
X,
(UniCl (FinMeetCl A)) #)
by A2;
:: according to PRE_TOPC:def 1 :: thesis: ( ( for b1 being Element of bool (bool 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 bool 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;
:: thesis: for b1, b2 being Element of bool 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
a,
b being
Subset of
TopStruct(#
X,
(UniCl (FinMeetCl A)) #) st
a in the
topology of
TopStruct(#
X,
(UniCl (FinMeetCl A)) #) &
b in the
topology of
TopStruct(#
X,
(UniCl (FinMeetCl A)) #) holds
a /\ b in the
topology of
TopStruct(#
X,
(UniCl (FinMeetCl A)) #)
by A1;
:: thesis: verum end;