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 A1: 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 )
consider S being correct Lawson TopAugmentation of T;
L1 = the topology of S by A1;
hence ( ex S being correct Lawson TopAugmentation of T st not L2 = the topology of S or L1 = L2 ) ; :: thesis: verum