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
( RelStr(# the carrier of T1,the InternalRel of T1 #) = RelStr(# the carrier of L,the InternalRel of L #) & 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 Th60; :: thesis: verum