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 ; :: thesis: for S being correct Lawson TopAugmentation of T holds t = the topology of S
let S9 be correct Lawson TopAugmentation of T; :: thesis: 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 ;
:: thesis: verum