let T1, T2 be non empty TopSpace; :: thesis: ( the carrier of T1 = the carrier of T2 implies for T being Refinement of T1,T2
for B1 being prebasis of T1
for B2 being prebasis of T2 holds B1 \/ B2 is prebasis of T )
assume A1: the carrier of T1 = the carrier of T2 ; :: thesis: for T being Refinement of T1,T2
for B1 being prebasis of T1
for B2 being prebasis of T2 holds B1 \/ B2 is prebasis of T
let T be Refinement of T1,T2; :: thesis: for B1 being prebasis of T1
for B2 being prebasis of T2 holds B1 \/ B2 is prebasis of T
A2: the carrier of T = the carrier of T1 \/ the carrier of T2 by YELLOW_9:def 6
.= the carrier of T1 by A1 ;
let B1 be prebasis of T1; :: thesis: for B2 being prebasis of T2 holds B1 \/ B2 is prebasis of T
let B2 be prebasis of T2; :: thesis: B1 \/ B2 is prebasis of T
{the carrier of T1,the carrier of T2} = {the carrier of T} by A1, A2, ENUMSET1:69;
then reconsider K = (B1 \/ B2) \/ {the carrier of T} as prebasis of T by YELLOW_9:58;
B1 \/ B2 c= K by XBOOLE_1:7;
then reconsider K' = B1 \/ B2 as Subset-Family of T by XBOOLE_1:1;
FinMeetCl K' = FinMeetCl K

proof

thus FinMeetCl K' c= FinMeetCl K by CANTOR_1:16, XBOOLE_1:7; :: according to XBOOLE_0:def 10 :: thesis: FinMeetCl K c= FinMeetCl K'
K c= FinMeetCl K'

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in K or a in FinMeetCl K' )
assume a in K ; :: thesis: a in FinMeetCl K'
then ( ( a in K' & K' c= FinMeetCl K' ) or ( a in {the carrier of T} & the carrier of T in FinMeetCl K' ) ) by CANTOR_1:4, CANTOR_1:8, XBOOLE_0:def 3;
hence a in FinMeetCl K' by TARSKI:def 1; :: thesis: verum

end;

then FinMeetCl K c= FinMeetCl (FinMeetCl K') by CANTOR_1:16;
hence FinMeetCl K c= FinMeetCl K' by CANTOR_1:13; :: thesis: verum

end;

then FinMeetCl K' is Basis of T by YELLOW_9:23;
hence B1 \/ B2 is prebasis of T by YELLOW_9:23; :: thesis: verum