let T be non empty TopSpace; :: thesis: for K, O being set st K c= O & O c= the topology of T holds
( ( K is Basis of T implies O is Basis of T ) & ( K is prebasis of T implies O is prebasis of T ) )
let K, O be set ; :: thesis: ( K c= O & O c= the topology of T implies ( ( K is Basis of T implies O is Basis of T ) & ( K is prebasis of T implies O is prebasis of T ) ) )
assume that
A1: K c= O and
A2: O c= the topology of T ; :: thesis: ( ( K is Basis of T implies O is Basis of T ) & ( K is prebasis of T implies O is prebasis of T ) )
K c= the topology of T by A1, A2;
then reconsider K9 = K, O9 = O as Subset-Family of T by A2, XBOOLE_1:1;
reconsider K9 = K9, O9 = O9 as Subset-Family of T ;
reconsider K9 = K9, O9 = O9 as Subset-Family of T ;
A3: UniCl K9 c= UniCl O9 by A1, CANTOR_1:9;
A4: UniCl the topology of T = the topology of T by CANTOR_1:6;
then A5: UniCl O9 c= the topology of T by A2, CANTOR_1:9;
hereby :: thesis: ( K is prebasis of T implies O is prebasis of T )
assume K is Basis of T ; :: thesis: O is Basis of T
then UniCl K9 = the topology of T by YELLOW_9:22;
then UniCl O9 = the topology of T by A5, A3;
hence O is Basis of T by YELLOW_9:22; :: thesis: verum
end;
FinMeetCl the topology of T = the topology of T by CANTOR_1:5;
then FinMeetCl O9 c= the topology of T by A2, CANTOR_1:14;
then A6: UniCl (FinMeetCl O9) c= the topology of T by A4, CANTOR_1:9;
assume K is prebasis of T ; :: thesis: O is prebasis of T
then FinMeetCl K9 is Basis of T by YELLOW_9:23;
then A7: UniCl (FinMeetCl K9) = the topology of T by YELLOW_9:22;
FinMeetCl K9 c= FinMeetCl O9 by A1, CANTOR_1:14;
then UniCl (FinMeetCl K9) c= UniCl (FinMeetCl O9) by CANTOR_1:9;
then UniCl (FinMeetCl O9) = the topology of T by A7, A6;
then FinMeetCl O9 is Basis of T by YELLOW_9:22;
hence O is prebasis of T by YELLOW_9:23; :: thesis: verum