let LL be non empty RelStr ; :: thesis: ex T being correct strict TopAugmentation of LL st T is lower
set A = { ((uparrow x) ` ) where x is Element of LL : verum } ;
{ ((uparrow x) ` ) where x is Element of LL : verum } c= bool the carrier of LL
then reconsider A = { ((uparrow x) ` ) where x is Element of LL : verum } as Subset-Family of LL ;
set T = TopRelStr(# the carrier of LL,the InternalRel of LL,(UniCl (FinMeetCl A)) #);
reconsider S = TopStruct(# the carrier of LL,(UniCl (FinMeetCl A)) #) as non empty TopSpace by CANTOR_1:17;
A1:
TopStruct(# the carrier of TopRelStr(# the carrier of LL,the InternalRel of LL,(UniCl (FinMeetCl A)) #),the topology of TopRelStr(# the carrier of LL,the InternalRel of LL,(UniCl (FinMeetCl A)) #) #) = S
;
TopRelStr(# the carrier of LL,the InternalRel of LL,(UniCl (FinMeetCl A)) #) is TopSpace-like
proof
thus
the
carrier of
TopRelStr(# the
carrier of
LL,the
InternalRel of
LL,
(UniCl (FinMeetCl A)) #)
in the
topology of
TopRelStr(# the
carrier of
LL,the
InternalRel of
LL,
(UniCl (FinMeetCl A)) #)
by A1, PRE_TOPC:def 1;
:: according to PRE_TOPC:def 1 :: thesis: ( ( for b1 being Element of bool (bool the carrier of TopRelStr(# the carrier of LL,the InternalRel of LL,(UniCl (FinMeetCl A)) #)) holds
( not b1 c= the topology of TopRelStr(# the carrier of LL,the InternalRel of LL,(UniCl (FinMeetCl A)) #) or union b1 in the topology of TopRelStr(# the carrier of LL,the InternalRel of LL,(UniCl (FinMeetCl A)) #) ) ) & ( for b1, b2 being Element of bool the carrier of TopRelStr(# the carrier of LL,the InternalRel of LL,(UniCl (FinMeetCl A)) #) holds
( not b1 in the topology of TopRelStr(# the carrier of LL,the InternalRel of LL,(UniCl (FinMeetCl A)) #) or not b2 in the topology of TopRelStr(# the carrier of LL,the InternalRel of LL,(UniCl (FinMeetCl A)) #) or b1 /\ b2 in the topology of TopRelStr(# the carrier of LL,the InternalRel of LL,(UniCl (FinMeetCl A)) #) ) ) )
hereby :: thesis: for b1, b2 being Element of bool the carrier of TopRelStr(# the carrier of LL,the InternalRel of LL,(UniCl (FinMeetCl A)) #) holds
( not b1 in the topology of TopRelStr(# the carrier of LL,the InternalRel of LL,(UniCl (FinMeetCl A)) #) or not b2 in the topology of TopRelStr(# the carrier of LL,the InternalRel of LL,(UniCl (FinMeetCl A)) #) or b1 /\ b2 in the topology of TopRelStr(# the carrier of LL,the InternalRel of LL,(UniCl (FinMeetCl A)) #) )
let a be
Subset-Family of
TopRelStr(# the
carrier of
LL,the
InternalRel of
LL,
(UniCl (FinMeetCl A)) #);
:: thesis: ( a c= the topology of TopRelStr(# the carrier of LL,the InternalRel of LL,(UniCl (FinMeetCl A)) #) implies union a in the topology of TopRelStr(# the carrier of LL,the InternalRel of LL,(UniCl (FinMeetCl A)) #) )reconsider b =
a as
Subset-Family of
S ;
assume
a c= the
topology of
TopRelStr(# the
carrier of
LL,the
InternalRel of
LL,
(UniCl (FinMeetCl A)) #)
;
:: thesis: union a in the topology of TopRelStr(# the carrier of LL,the InternalRel of LL,(UniCl (FinMeetCl A)) #)then
union b in the
topology of
S
by PRE_TOPC:def 1;
hence
union a in the
topology of
TopRelStr(# the
carrier of
LL,the
InternalRel of
LL,
(UniCl (FinMeetCl A)) #)
;
:: thesis: verum
end;
let a,
b be
Subset of
TopRelStr(# the
carrier of
LL,the
InternalRel of
LL,
(UniCl (FinMeetCl A)) #);
:: thesis: ( not a in the topology of TopRelStr(# the carrier of LL,the InternalRel of LL,(UniCl (FinMeetCl A)) #) or not b in the topology of TopRelStr(# the carrier of LL,the InternalRel of LL,(UniCl (FinMeetCl A)) #) or a /\ b in the topology of TopRelStr(# the carrier of LL,the InternalRel of LL,(UniCl (FinMeetCl A)) #) )
assume
(
a in the
topology of
TopRelStr(# the
carrier of
LL,the
InternalRel of
LL,
(UniCl (FinMeetCl A)) #) &
b in the
topology of
TopRelStr(# the
carrier of
LL,the
InternalRel of
LL,
(UniCl (FinMeetCl A)) #) )
;
:: thesis: a /\ b in the topology of TopRelStr(# the carrier of LL,the InternalRel of LL,(UniCl (FinMeetCl A)) #)
then
a /\ b in the
topology of
S
by PRE_TOPC:def 1;
hence
a /\ b in the
topology of
TopRelStr(# the
carrier of
LL,the
InternalRel of
LL,
(UniCl (FinMeetCl A)) #)
;
:: thesis: verum
end;
then reconsider T = TopRelStr(# the carrier of LL,the InternalRel of LL,(UniCl (FinMeetCl A)) #) as non empty TopSpace-like strict TopRelStr ;
take
T
; :: thesis: ( T is correct strict TopAugmentation of LL & T is lower )
RelStr(# the carrier of T,the InternalRel of T #) = RelStr(# the carrier of LL,the InternalRel of LL #)
;
hence
T is correct strict TopAugmentation of LL
by YELLOW_9:def 4; :: thesis: T is lower
A2:
A is prebasis of S
by CANTOR_1:20;
then A3:
A c= the topology of S
by CANTOR_1:def 5;
consider F being Basis of S such that
A4:
F c= FinMeetCl A
by A2, CANTOR_1:def 5;
set BB = { ((uparrow x) ` ) where x is Element of T : verum } ;
RelStr(# the carrier of T,the InternalRel of T #) = RelStr(# the carrier of LL,the InternalRel of LL #)
;
then A5:
A = { ((uparrow x) ` ) where x is Element of T : verum }
by Lm1;
( F c= the topology of T & the topology of T c= UniCl F )
by CANTOR_1:def 2;
then
F is Basis of T
by CANTOR_1:def 2;
hence
{ ((uparrow x) ` ) where x is Element of T : verum } is prebasis of T
by A3, A4, A5, CANTOR_1:def 5; :: according to WAYBEL19:def 1 :: thesis: verum