let T1, T2 be non empty TopSpace; :: thesis: ( the carrier of T1 = the carrier of T2 implies for T being Refinement of T1,T2 holds INTERSECTION ( the topology of T1, the topology of T2) is Basis of T )
assume A1: the carrier of T1 = the carrier of T2 ; :: thesis: for T being Refinement of T1,T2 holds INTERSECTION ( the topology of T1, the topology of T2) is Basis of T
let T be Refinement of T1,T2; :: thesis: INTERSECTION ( the topology of T1, the topology of T2) is Basis of T
set B1 = the topology of T1;
set B2 = the topology of T2;
UniCl the topology of T1 = the topology of T1 by CANTOR_1:6;
then reconsider B1 = the topology of T1 as Basis of T1 by Th22;
UniCl the topology of T2 = the topology of T2 by CANTOR_1:6;
then reconsider B2 = the topology of T2 as Basis of T2 by Th22;
A2: (B1 \/ B2) \/ (INTERSECTION (B1,B2)) is Basis of T by Th59;
A3: the carrier of T1 in B1 by PRE_TOPC:def 1;
A4: the carrier of T2 in B2 by PRE_TOPC:def 1;
A5: B1 c= INTERSECTION (B1,B2)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in B1 or a in INTERSECTION (B1,B2) )
reconsider aa = a as set by TARSKI:1;
assume A6: a in B1 ; :: thesis: a in INTERSECTION (B1,B2)
then aa /\ the carrier of T1 in INTERSECTION (B1,B2) by A1, A4, SETFAM_1:def 5;
hence a in INTERSECTION (B1,B2) by A6, XBOOLE_1:28; :: thesis: verum

end;

B2 c= INTERSECTION (B1,B2)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in B2 or a in INTERSECTION (B1,B2) )
reconsider aa = a as set by TARSKI:1;
assume A7: a in B2 ; :: thesis: a in INTERSECTION (B1,B2)
then aa /\ the carrier of T2 in INTERSECTION (B1,B2) by A1, A3, SETFAM_1:def 5;
hence a in INTERSECTION (B1,B2) by A7, XBOOLE_1:28; :: thesis: verum

end;

hence INTERSECTION ( the topology of T1, the topology of T2) is Basis of T by A2, A5, XBOOLE_1:8, XBOOLE_1:12; :: thesis: verum