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