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 A1: ( K c= O & 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 ) )
then K c= the topology of T by XBOOLE_1:1;
then reconsider K' = K, O' = O as Subset-Family of T by A1, XBOOLE_1:1;
reconsider K' = K', O' = O' as Subset-Family of T ;
reconsider K' = K', O' = O' as Subset-Family of T ;
A2: ( FinMeetCl the topology of T = the topology of T & UniCl the topology of T = the topology of T ) by CANTOR_1:5, CANTOR_1:6;
then A3: ( UniCl O' c= the topology of T & UniCl K' c= UniCl O' ) by A1, CANTOR_1:9;
( FinMeetCl O' c= the topology of T & FinMeetCl K' c= FinMeetCl O' ) by A1, A2, CANTOR_1:16;
then A4: ( UniCl (FinMeetCl O') c= the topology of T & UniCl (FinMeetCl K') c= UniCl (FinMeetCl O') ) 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 K' = the topology of T by YELLOW_9:22;
then UniCl O' = the topology of T by A3, XBOOLE_0:def 10;
hence O is Basis of T by YELLOW_9:22; :: thesis: verum

end;

assume K is prebasis of T ; :: thesis: O is prebasis of T
then FinMeetCl K' is Basis of T by YELLOW_9:23;
then UniCl (FinMeetCl K') = the topology of T by YELLOW_9:22;
then UniCl (FinMeetCl O') = the topology of T by A4, XBOOLE_0:def 10;
then FinMeetCl O' is Basis of T by YELLOW_9:22;
hence O is prebasis of T by YELLOW_9:23; :: thesis: verum