consider S being correct Lawson TopAugmentation of T;
A1: RelStr(# the carrier of S,the InternalRel of S #) = RelStr(# the carrier of T,the InternalRel of T #) by YELLOW_9:def 4;
then reconsider t = the topology of S 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 S 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 S by A2, A1, Th3;
(omega S) \/ (sigma S) is prebasis of S by Def3;
then FinMeetCl ((omega S) \/ (sigma S)) is Basis of S by YELLOW_9:23;
hence t = UniCl (FinMeetCl ((omega S) \/ (sigma S))) by YELLOW_9:22
.= the topology of S9 by A1, A2, A5, A3, A4, YELLOW_9:22 ;
:: thesis: verum