let S, T be TopSpace; :: thesis: ( [#] S c= [#] T & ex K being prebasis of S ex L being prebasis of T st K = INTERSECTION (L,{([#] S)}) implies S is SubSpace of T )
assume A1: [#] S c= [#] T ; :: thesis: ( for K being prebasis of S
for L being prebasis of T holds not K = INTERSECTION (L,{([#] S)}) or S is SubSpace of T )

given K being prebasis of S, L being prebasis of T such that A2: K = INTERSECTION (L,{([#] S)}) ; :: thesis: S is SubSpace of T
reconsider K0 = FinMeetCl K as Basis of S by YELLOW_9:23;
reconsider L0 = FinMeetCl L as Basis of T by YELLOW_9:23;
for x being object holds
( x in K0 iff x in INTERSECTION (L0,{([#] S)}) )
proof
let x be object ; :: thesis: ( x in K0 iff x in INTERSECTION (L0,{([#] S)}) )
hereby :: thesis: ( x in INTERSECTION (L0,{([#] S)}) implies x in K0 )
assume A3: x in K0 ; :: thesis: x in INTERSECTION (L0,{([#] S)})
then reconsider A = x as Subset of S ;
consider X being Subset-Family of S such that
A4: ( X c= K & X is finite & A = Intersect X ) by ;
per cases ( X <> {} or X = {} ) ;
suppose A5: X <> {} ; :: thesis: x in INTERSECTION (L0,{([#] S)})
then A6: A = meet X by ;
defpred S1[ object , object ] means ex D being Subset of T st
( \$1 = D /\ ([#] S) & \$2 = D );
A7: for x being object st x in X holds
ex y being object st
( y in L & S1[x,y] )
proof
let x be object ; :: thesis: ( x in X implies ex y being object st
( y in L & S1[x,y] ) )

assume x in X ; :: thesis: ex y being object st
( y in L & S1[x,y] )

then consider D, S0 being set such that
A8: ( D in L & S0 in {([#] S)} & x = D /\ S0 ) by ;
take D ; :: thesis: ( D in L & S1[x,D] )
thus D in L by A8; :: thesis: S1[x,D]
reconsider D0 = D as Subset of T by A8;
take D0 ; :: thesis: ( x = D0 /\ ([#] S) & D = D0 )
thus ( x = D0 /\ ([#] S) & D = D0 ) by ; :: thesis: verum
end;
consider f being Function such that
A9: ( dom f = X & rng f c= L ) and
A10: for x being object st x in X holds
S1[x,f . x] from reconsider Y = rng f as Subset-Family of T by ;
set B = meet Y;
A11: Y is finite by ;
A12: f <> {} by A5, A9;
then meet Y = Intersect Y by SETFAM_1:def 9;
then A13: meet Y in L0 by ;
for y being object holds
( y in A iff y in (meet Y) /\ ([#] S) )
proof
let y be object ; :: thesis: ( y in A iff y in (meet Y) /\ ([#] S) )
hereby :: thesis: ( y in (meet Y) /\ ([#] S) implies y in A )
assume A14: y in A ; :: thesis: y in (meet Y) /\ ([#] S)
for D being set st D in Y holds
y in D
proof
let D be set ; :: thesis: ( D in Y implies y in D )
assume D in Y ; :: thesis: y in D
then consider C being object such that
A15: ( C in dom f & f . C = D ) by FUNCT_1:def 3;
reconsider C = C as set by TARSKI:1;
A16: ex D0 being Subset of T st
( C = D0 /\ ([#] S) & D = D0 ) by A9, A10, A15;
y in C by ;
hence y in D by ; :: thesis: verum
end;
then A17: y in meet Y by ;
the carrier of S = [#] S by STRUCT_0:def 3;
hence y in (meet Y) /\ ([#] S) by ; :: thesis: verum
end;
assume y in (meet Y) /\ ([#] S) ; :: thesis: y in A
then A18: ( y in meet Y & y in [#] S ) by XBOOLE_0:def 4;
for C being set st C in X holds
y in C
proof
let C be set ; :: thesis: ( C in X implies y in C )
assume A19: C in X ; :: thesis: y in C
then consider D being Subset of T such that
A20: ( C = D /\ ([#] S) & f . C = D ) by A10;
D in Y by ;
then y in D by ;
hence y in C by ; :: thesis: verum
end;
hence y in A by ; :: thesis: verum
end;
then A21: A = (meet Y) /\ ([#] S) by TARSKI:2;
[#] S in {([#] S)} by TARSKI:def 1;
hence x in INTERSECTION (L0,{([#] S)}) by ; :: thesis: verum
end;
suppose X = {} ; :: thesis: x in INTERSECTION (L0,{([#] S)})
then A22: A = the carrier of S by
.= [#] S by STRUCT_0:def 3 ;
ex B, S0 being set st
( B in L0 & S0 in {([#] S)} & A = B /\ S0 )
proof
take [#] T ; :: thesis: ex S0 being set st
( [#] T in L0 & S0 in {([#] S)} & A = ([#] T) /\ S0 )

take [#] S ; :: thesis: ( [#] T in L0 & [#] S in {([#] S)} & A = ([#] T) /\ ([#] S) )
set Y = the empty Subset-Family of T;
A23: ( the empty Subset-Family of T c= L & the empty Subset-Family of T is finite ) by XBOOLE_1:2;
Intersect the empty Subset-Family of T = the carrier of T by SETFAM_1:def 9
.= [#] T by STRUCT_0:def 3 ;
hence ( [#] T in L0 & [#] S in {([#] S)} & A = ([#] T) /\ ([#] S) ) by ; :: thesis: verum
end;
hence x in INTERSECTION (L0,{([#] S)}) by SETFAM_1:def 5; :: thesis: verum
end;
end;
end;
assume x in INTERSECTION (L0,{([#] S)}) ; :: thesis: x in K0
then consider B, S0 being set such that
A24: ( B in L0 & S0 in {([#] S)} & x = B /\ S0 ) by SETFAM_1:def 5;
consider Y being Subset-Family of T such that
A25: ( Y c= L & Y is finite & B = Intersect Y ) by ;
per cases ( Y <> {} or Y = {} ) ;
suppose A26: Y <> {} ; :: thesis: x in K0
defpred S1[ object , object ] means ex D being Subset of T st
( \$2 = D /\ ([#] S) & \$1 = D );
A27: for x being object st x in Y holds
ex y being object st
( y in K & S1[x,y] )
proof
let x be object ; :: thesis: ( x in Y implies ex y being object st
( y in K & S1[x,y] ) )

assume A28: x in Y ; :: thesis: ex y being object st
( y in K & S1[x,y] )

then reconsider D = x as Subset of T ;
take D /\ ([#] S) ; :: thesis: ( D /\ ([#] S) in K & S1[x,D /\ ([#] S)] )
[#] S in {([#] S)} by TARSKI:def 1;
hence D /\ ([#] S) in K by ; :: thesis: S1[x,D /\ ([#] S)]
take D ; :: thesis: ( D /\ ([#] S) = D /\ ([#] S) & x = D )
thus ( D /\ ([#] S) = D /\ ([#] S) & x = D ) ; :: thesis: verum
end;
consider f being Function such that
A29: ( dom f = Y & rng f c= K ) and
A30: for x being object st x in Y holds
S1[x,f . x] from reconsider X = rng f as Subset-Family of S by ;
A31: X is finite by ;
a32: f <> {} by ;
reconsider A = x as set by TARSKI:1;
for y being object holds
( y in A iff for M being set st M in X holds
y in M )
proof
let y be object ; :: thesis: ( y in A iff for M being set st M in X holds
y in M )

hereby :: thesis: ( ( for M being set st M in X holds
y in M ) implies y in A )
assume A33: y in A ; :: thesis: for M being set st M in X holds
y in M

let M be set ; :: thesis: ( M in X implies y in M )
assume M in X ; :: thesis: y in M
then consider D being object such that
A34: ( D in dom f & f . D = M ) by FUNCT_1:def 3;
consider D0 being Subset of T such that
A35: ( M = D0 /\ ([#] S) & D = D0 ) by ;
y in B by ;
then y in meet Y by ;
then A36: y in D0 by ;
y in S0 by ;
then y in [#] S by ;
hence y in M by ; :: thesis: verum
end;
assume A37: for M being set st M in X holds
y in M ; :: thesis: y in A
for M being set st M in Y holds
y in M
proof
let M be set ; :: thesis: ( M in Y implies y in M )
assume A38: M in Y ; :: thesis: y in M
then consider D being Subset of T such that
A39: ( f . M = D /\ ([#] S) & M = D ) by A30;
M /\ ([#] S) in X by ;
then y in M /\ ([#] S) by A37;
hence y in M by ; :: thesis: verum
end;
then y in meet Y by ;
then A40: y in B by ;
set M0 = the Element of Y;
consider D0 being Subset of T such that
A41: ( f . the Element of Y = D0 /\ ([#] S) & the Element of Y = D0 ) by ;
the Element of Y /\ ([#] S) in X by ;
then y in the Element of Y /\ ([#] S) by A37;
then y in [#] S by ;
then y in S0 by ;
hence y in A by ; :: thesis: verum
end;
then A = meet X by ;
then x = Intersect X by ;
hence x in K0 by ; :: thesis: verum
end;
suppose Y = {} ; :: thesis: x in K0
then A42: B = the carrier of T by
.= [#] T by STRUCT_0:def 3 ;
set X = the empty Subset-Family of S;
[#] S = the carrier of S by STRUCT_0:def 3;
then a43: ( the empty Subset-Family of S c= K & the empty Subset-Family of S is finite & [#] S = Intersect the empty Subset-Family of S ) by ;
x = B /\ ([#] S) by
.= [#] S by ;
hence x in K0 by ; :: thesis: verum
end;
end;
end;
hence S is SubSpace of T by ; :: thesis: verum