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
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 T = the carrier of T1 \/ the carrier of T2 by YELLOW_9:def 6
.= the carrier of T1 by A1 ;
then { the carrier of T1, the carrier of T2} = { the carrier of T} by A1, ENUMSET1:29;
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 K9 = B1 \/ B2 as Subset-Family of T by XBOOLE_1:1;
K c= FinMeetCl K9
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in K or a in FinMeetCl K9 )
assume a in K ; :: thesis: a in FinMeetCl K9
then ( ( a in K9 & K9 c= FinMeetCl K9 ) or ( a in { the carrier of T} & the carrier of T in FinMeetCl K9 ) ) by CANTOR_1:4, CANTOR_1:8, XBOOLE_0:def 3;
hence a in FinMeetCl K9 by TARSKI:def 1; :: thesis: verum
end;
then FinMeetCl K c= FinMeetCl (FinMeetCl K9) by CANTOR_1:14;
then A2: FinMeetCl K c= FinMeetCl K9 by CANTOR_1:11;
FinMeetCl K9 c= FinMeetCl K by CANTOR_1:14, XBOOLE_1:7;
then FinMeetCl K9 = FinMeetCl K by A2;
then FinMeetCl K9 is Basis of T by YELLOW_9:23;
hence B1 \/ B2 is prebasis of T by YELLOW_9:23; :: thesis: verum