let L be non empty RelStr ; :: thesis: for T1, T2 being correct TopAugmentation of L
for T being Refinement of T1,T2 holds INTERSECTION the topology of T1,the topology of T2 is Basis of T
let T1, T2 be correct TopAugmentation of L; :: thesis: for T being Refinement of T1,T2 holds INTERSECTION the topology of T1,the topology of T2 is Basis of T
A1: RelStr(# the carrier of T1,the InternalRel of T1 #) = RelStr(# the carrier of L,the InternalRel of L #) by Def4;
RelStr(# the carrier of T2,the InternalRel of T2 #) = RelStr(# the carrier of L,the InternalRel of L #) by Def4;
hence for T being Refinement of T1,T2 holds INTERSECTION the topology of T1,the topology of T2 is Basis of T by A1, Th60; :: thesis: verum