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