set S = the correct Lawson TopAugmentation of T;
let L1, L2 be Subset-Family of T; :: thesis: ( ( for S being correct Lawson TopAugmentation of T holds L1 = the topology of S ) & ( for S being correct Lawson TopAugmentation of T holds L2 = the topology of S ) implies L1 = L2 )
assume for S being correct Lawson TopAugmentation of T holds L1 = the topology of S ; :: thesis: ( ex S being correct Lawson TopAugmentation of T st not L2 = the topology of S or L1 = L2 )
then L1 = the topology of the correct Lawson TopAugmentation of T ;
hence ( ex S being correct Lawson TopAugmentation of T st not L2 = the topology of S or L1 = L2 ) ; :: thesis: verum