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 ;
take t ; :: thesis: for S being correct Lawson TopAugmentation of T holds t = the topology of S
let S' be correct Lawson TopAugmentation of T; :: thesis: t = the topology of S'
A2: RelStr(# the carrier of S',the InternalRel of S' #) = RelStr(# the carrier of T,the InternalRel of T #) by YELLOW_9:def 4;
then A3: sigma S' = sigma S by A1, YELLOW_9:52;
(omega S') \/ (sigma S') is prebasis of S' by Def3;
then A4: FinMeetCl ((omega S') \/ (sigma S')) is Basis of S' by YELLOW_9:23;
A5: omega S' = 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 S' by A1, A2, A5, A3, A4, YELLOW_9:22 ;
:: thesis: verum