set S = the correct Lawson TopAugmentation of T;
A1:
RelStr(# the carrier of the correct Lawson TopAugmentation of T, the InternalRel of the correct Lawson TopAugmentation of T #) = RelStr(# the carrier of T, the InternalRel of T #)
by YELLOW_9:def 4;
then reconsider t = the topology of the correct Lawson TopAugmentation of T as Subset-Family of T ;
take
t
; for S being correct Lawson TopAugmentation of T holds t = the topology of S
let S9 be correct Lawson TopAugmentation of T; t = the topology of S9
A2:
RelStr(# the carrier of S9, the InternalRel of S9 #) = RelStr(# the carrier of T, the InternalRel of T #)
by YELLOW_9:def 4;
then A3:
sigma S9 = sigma the correct Lawson TopAugmentation of T
by A1, YELLOW_9:52;
(omega S9) \/ (sigma S9) is prebasis of S9
by Def3;
then A4:
FinMeetCl ((omega S9) \/ (sigma S9)) is Basis of S9
by YELLOW_9:23;
A5:
omega S9 = omega the correct Lawson TopAugmentation of T
by A2, A1, Th3;
(omega the correct Lawson TopAugmentation of T) \/ (sigma the correct Lawson TopAugmentation of T) is prebasis of the correct Lawson TopAugmentation of T
by Def3;
then
FinMeetCl ((omega the correct Lawson TopAugmentation of T) \/ (sigma the correct Lawson TopAugmentation of T)) is Basis of the correct Lawson TopAugmentation of T
by YELLOW_9:23;
hence t =
UniCl (FinMeetCl ((omega the correct Lawson TopAugmentation of T) \/ (sigma the correct Lawson TopAugmentation of T)))
by YELLOW_9:22
.=
the topology of S9
by A1, A2, A5, A3, A4, YELLOW_9:22
;
verum