let X be non empty 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
set T = TopStruct(# X,(UniCl (FinMeetCl A)) #);
A1:
[#] TopStruct(# X,(UniCl (FinMeetCl A)) #) in FinMeetCl A
by Th8;
hence
the carrier of TopStruct(# X,(UniCl (FinMeetCl A)) #) in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #)
by Def1; PRE_TOPC:def 1 ( ( 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)) #) ) ) )
thus
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)) #)
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)) #) )
let a, b be Subset of TopStruct(# X,(UniCl (FinMeetCl A)) #); ( not a in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) or not b in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) or a /\ b in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) )
assume
a in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #)
; ( not b in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) or a /\ b in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) )
then consider F being Subset-Family of X such that
A10:
F c= FinMeetCl A
and
A11:
a = union F
by Def1;
assume
b in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #)
; a /\ b in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #)
then consider G being Subset-Family of X such that
A12:
G c= FinMeetCl A
and
A13:
b = union G
by Def1;
A14:
union (INTERSECTION (F,G)) = a /\ b
by A11, A13, SETFAM_1:28;
A15:
INTERSECTION (F,G) c= FinMeetCl A
by A10, A12, Th13;
then
INTERSECTION (F,G) is Subset-Family of X
by XBOOLE_1:1;
hence
a /\ b in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #)
by A15, A14, Def1; verum