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)}) )

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

hence
S is SubSpace of T
by TARSKI:2, Th49; :: thesis: verum
let x be object ; :: thesis: ( x in K0 iff x in INTERSECTION (L0,{([#] S)}) )

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 A24, CANTOR_1:def 3;

end;hereby :: thesis: ( x in INTERSECTION (L0,{([#] S)}) implies x in K0 )

assume
x in INTERSECTION (L0,{([#] S)})
; :: thesis: x in K0assume 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 A3, CANTOR_1:def 3;

end;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 A3, CANTOR_1:def 3;

per cases
( X <> {} or X = {} )
;

end;

suppose A5:
X <> {}
; :: thesis: x in INTERSECTION (L0,{([#] S)})

then A6:
A = meet X
by A4, SETFAM_1:def 9;

defpred S_{1}[ 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 & S_{1}[x,y] )

A9: ( dom f = X & rng f c= L ) and

A10: for x being object st x in X holds

S_{1}[x,f . x]
from FUNCT_1:sch 6(A7);

reconsider Y = rng f as Subset-Family of T by A9, XBOOLE_1:1;

set B = meet Y;

A11: Y is finite by A4, A9, FINSET_1:8;

A12: f <> {} by A5, A9;

then meet Y = Intersect Y by SETFAM_1:def 9;

then A13: meet Y in L0 by A9, A11, CANTOR_1:def 3;

for y being object holds

( y in A iff y in (meet Y) /\ ([#] S) )

[#] S in {([#] S)} by TARSKI:def 1;

hence x in INTERSECTION (L0,{([#] S)}) by A13, A21, SETFAM_1:def 5; :: thesis: verum

end;defpred S

( $1 = D /\ ([#] S) & $2 = D );

A7: for x being object st x in X holds

ex y being object st

( y in L & S

proof

consider f being Function such that
let x be object ; :: thesis: ( x in X implies ex y being object st

( y in L & S_{1}[x,y] ) )

assume x in X ; :: thesis: ex y being object st

( y in L & S_{1}[x,y] )

then consider D, S0 being set such that

A8: ( D in L & S0 in {([#] S)} & x = D /\ S0 ) by A2, A4, SETFAM_1:def 5;

take D ; :: thesis: ( D in L & S_{1}[x,D] )

thus D in L by A8; :: thesis: S_{1}[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 A8, TARSKI:def 1; :: thesis: verum

end;( y in L & S

assume x in X ; :: thesis: ex y being object st

( y in L & S

then consider D, S0 being set such that

A8: ( D in L & S0 in {([#] S)} & x = D /\ S0 ) by A2, A4, SETFAM_1:def 5;

take D ; :: thesis: ( D in L & S

thus D in L by A8; :: thesis: S

reconsider D0 = D as Subset of T by A8;

take D0 ; :: thesis: ( x = D0 /\ ([#] S) & D = D0 )

thus ( x = D0 /\ ([#] S) & D = D0 ) by A8, TARSKI:def 1; :: thesis: verum

A9: ( dom f = X & rng f c= L ) and

A10: for x being object st x in X holds

S

reconsider Y = rng f as Subset-Family of T by A9, XBOOLE_1:1;

set B = meet Y;

A11: Y is finite by A4, A9, FINSET_1:8;

A12: f <> {} by A5, A9;

then meet Y = Intersect Y by SETFAM_1:def 9;

then A13: meet Y in L0 by A9, A11, CANTOR_1:def 3;

for y being object holds

( y in A iff y in (meet Y) /\ ([#] S) )

proof

then A21:
A = (meet Y) /\ ([#] S)
by TARSKI:2;
let y be object ; :: thesis: ( y in A iff y in (meet Y) /\ ([#] S) )

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

end;hereby :: thesis: ( y in (meet Y) /\ ([#] S) implies y in A )

assume
y in (meet Y) /\ ([#] S)
; :: thesis: y in Aassume A14:
y in A
; :: thesis: y in (meet Y) /\ ([#] S)

for D being set st D in Y holds

y in D

the carrier of S = [#] S by STRUCT_0:def 3;

hence y in (meet Y) /\ ([#] S) by A14, A17, XBOOLE_0:def 4; :: thesis: verum

end;for D being set st D in Y holds

y in D

proof

then A17:
y in meet Y
by A12, SETFAM_1:def 1;
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 A6, A9, A14, A15, SETFAM_1:def 1;

hence y in D by A16, TARSKI:def 3, XBOOLE_1:17; :: thesis: verum

end;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 A6, A9, A14, A15, SETFAM_1:def 1;

hence y in D by A16, TARSKI:def 3, XBOOLE_1:17; :: thesis: verum

the carrier of S = [#] S by STRUCT_0:def 3;

hence y in (meet Y) /\ ([#] S) by A14, A17, XBOOLE_0:def 4; :: thesis: verum

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

hence
y in A
by A5, A6, SETFAM_1:def 1; :: thesis: verum
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 A9, A19, A20, FUNCT_1:def 3;

then y in D by A18, SETFAM_1:def 1;

hence y in C by A18, A20, XBOOLE_0:def 4; :: thesis: verum

end;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 A9, A19, A20, FUNCT_1:def 3;

then y in D by A18, SETFAM_1:def 1;

hence y in C by A18, A20, XBOOLE_0:def 4; :: thesis: verum

[#] S in {([#] S)} by TARSKI:def 1;

hence x in INTERSECTION (L0,{([#] S)}) by A13, A21, SETFAM_1:def 5; :: thesis: verum

suppose
X = {}
; :: thesis: x in INTERSECTION (L0,{([#] S)})

then A22: A =
the carrier of S
by A4, SETFAM_1:def 9

.= [#] S by STRUCT_0:def 3 ;

ex B, S0 being set st

( B in L0 & S0 in {([#] S)} & A = B /\ S0 )

end;.= [#] S by STRUCT_0:def 3 ;

ex B, S0 being set st

( B in L0 & S0 in {([#] S)} & A = B /\ S0 )

proof

hence
x in INTERSECTION (L0,{([#] S)})
by SETFAM_1:def 5; :: thesis: verum
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 A1, A22, XBOOLE_1:28, TARSKI:def 1, A23, CANTOR_1:def 3; :: thesis: verum

end;( [#] 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 A1, A22, XBOOLE_1:28, TARSKI:def 1, A23, CANTOR_1:def 3; :: thesis: verum

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 A24, CANTOR_1:def 3;

per cases
( Y <> {} or Y = {} )
;

end;

suppose A26:
Y <> {}
; :: thesis: x in K0

defpred S_{1}[ 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 & S_{1}[x,y] )

A29: ( dom f = Y & rng f c= K ) and

A30: for x being object st x in Y holds

S_{1}[x,f . x]
from FUNCT_1:sch 6(A27);

reconsider X = rng f as Subset-Family of S by A29, XBOOLE_1:1;

A31: X is finite by A25, A29, FINSET_1:8;

a32: f <> {} by A26, A29;

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 )

then x = Intersect X by a32, SETFAM_1:def 9;

hence x in K0 by A29, A31, CANTOR_1:def 3; :: thesis: verum

end;( $2 = D /\ ([#] S) & $1 = D );

A27: for x being object st x in Y holds

ex y being object st

( y in K & S

proof

consider f being Function such that
let x be object ; :: thesis: ( x in Y implies ex y being object st

( y in K & S_{1}[x,y] ) )

assume A28: x in Y ; :: thesis: ex y being object st

( y in K & S_{1}[x,y] )

then reconsider D = x as Subset of T ;

take D /\ ([#] S) ; :: thesis: ( D /\ ([#] S) in K & S_{1}[x,D /\ ([#] S)] )

[#] S in {([#] S)} by TARSKI:def 1;

hence D /\ ([#] S) in K by A2, A25, A28, SETFAM_1:def 5; :: thesis: S_{1}[x,D /\ ([#] S)]

take D ; :: thesis: ( D /\ ([#] S) = D /\ ([#] S) & x = D )

thus ( D /\ ([#] S) = D /\ ([#] S) & x = D ) ; :: thesis: verum

end;( y in K & S

assume A28: x in Y ; :: thesis: ex y being object st

( y in K & S

then reconsider D = x as Subset of T ;

take D /\ ([#] S) ; :: thesis: ( D /\ ([#] S) in K & S

[#] S in {([#] S)} by TARSKI:def 1;

hence D /\ ([#] S) in K by A2, A25, A28, SETFAM_1:def 5; :: thesis: S

take D ; :: thesis: ( D /\ ([#] S) = D /\ ([#] S) & x = D )

thus ( D /\ ([#] S) = D /\ ([#] S) & x = D ) ; :: thesis: verum

A29: ( dom f = Y & rng f c= K ) and

A30: for x being object st x in Y holds

S

reconsider X = rng f as Subset-Family of S by A29, XBOOLE_1:1;

A31: X is finite by A25, A29, FINSET_1:8;

a32: f <> {} by A26, A29;

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

then
A = meet X
by a32, SETFAM_1:def 1;
let y be object ; :: thesis: ( y in A iff for M being set st M in X holds

y in M )

y in M ; :: thesis: y in A

for M being set st M in Y holds

y in M

then A40: y in B by A25, A26, SETFAM_1:def 9;

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 A26, A30;

the Element of Y /\ ([#] S) in X by A29, A26, A41, FUNCT_1:3;

then y in the Element of Y /\ ([#] S) by A37;

then y in [#] S by XBOOLE_1:17, TARSKI:def 3;

then y in S0 by A24, TARSKI:def 1;

hence y in A by A24, A40, XBOOLE_0:def 4; :: thesis: verum

end;y in M )

hereby :: thesis: ( ( for M being set st M in X holds

y in M ) implies y in A )

assume A37:
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 A29, A30, A34;

y in B by A24, A33, XBOOLE_0:def 4;

then y in meet Y by A25, A26, SETFAM_1:def 9;

then A36: y in D0 by A29, A34, A35, SETFAM_1:def 1;

y in S0 by A24, A33, XBOOLE_0:def 4;

then y in [#] S by A24, TARSKI:def 1;

hence y in M by A36, A35, XBOOLE_0:def 4; :: thesis: verum

end;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 A29, A30, A34;

y in B by A24, A33, XBOOLE_0:def 4;

then y in meet Y by A25, A26, SETFAM_1:def 9;

then A36: y in D0 by A29, A34, A35, SETFAM_1:def 1;

y in S0 by A24, A33, XBOOLE_0:def 4;

then y in [#] S by A24, TARSKI:def 1;

hence y in M by A36, A35, XBOOLE_0:def 4; :: thesis: verum

y in M ; :: thesis: y in A

for M being set st M in Y holds

y in M

proof

then
y in meet Y
by A26, SETFAM_1:def 1;
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 A29, A38, A39, FUNCT_1:3;

then y in M /\ ([#] S) by A37;

hence y in M by XBOOLE_1:17, TARSKI:def 3; :: thesis: verum

end;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 A29, A38, A39, FUNCT_1:3;

then y in M /\ ([#] S) by A37;

hence y in M by XBOOLE_1:17, TARSKI:def 3; :: thesis: verum

then A40: y in B by A25, A26, SETFAM_1:def 9;

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 A26, A30;

the Element of Y /\ ([#] S) in X by A29, A26, A41, FUNCT_1:3;

then y in the Element of Y /\ ([#] S) by A37;

then y in [#] S by XBOOLE_1:17, TARSKI:def 3;

then y in S0 by A24, TARSKI:def 1;

hence y in A by A24, A40, XBOOLE_0:def 4; :: thesis: verum

then x = Intersect X by a32, SETFAM_1:def 9;

hence x in K0 by A29, A31, CANTOR_1:def 3; :: thesis: verum

suppose
Y = {}
; :: thesis: x in K0

then A42: B =
the carrier of T
by A25, SETFAM_1:def 9

.= [#] 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 XBOOLE_1:2, SETFAM_1:def 9;

x = B /\ ([#] S) by A24, TARSKI:def 1

.= [#] S by A1, A42, XBOOLE_1:28 ;

hence x in K0 by a43, CANTOR_1:def 3; :: thesis: verum

end;.= [#] 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 XBOOLE_1:2, SETFAM_1:def 9;

x = B /\ ([#] S) by A24, TARSKI:def 1

.= [#] S by A1, A42, XBOOLE_1:28 ;

hence x in K0 by a43, CANTOR_1:def 3; :: thesis: verum