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