let S, T be TopSpace; ( [#] 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
; ( 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)})
; 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 ;
( x in K0 iff x in INTERSECTION (L0,{([#] S)}) )
hereby ( x in INTERSECTION (L0,{([#] S)}) implies x in K0 )
assume A3:
x in K0
;
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;
per cases
( X <> {} or X = {} )
;
suppose A5:
X <> {}
;
x in INTERSECTION (L0,{([#] S)})then A6:
A = meet X
by A4, SETFAM_1:def 9;
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] )
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 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) )
then A21:
A = (meet Y) /\ ([#] S)
by TARSKI:2;
[#] S in {([#] S)}
by TARSKI:def 1;
hence
x in INTERSECTION (
L0,
{([#] S)})
by A13, A21, SETFAM_1:def 5;
verum end; end;
end;
assume
x in INTERSECTION (
L0,
{([#] S)})
;
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 A24, CANTOR_1:def 3;
per cases
( Y <> {} or Y = {} )
;
suppose A26:
Y <> {}
;
x in K0defpred 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] )
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 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 )
proof
let y be
object ;
( y in A iff for M being set st M in X holds
y in M )
hereby ( ( for M being set st M in X holds
y in M ) implies y in A )
assume A33:
y in A
;
for M being set st M in X holds
y in Mlet M be
set ;
( M in X implies y in M )assume
M in X
;
y in Mthen 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;
verum
end;
assume A37:
for
M being
set st
M in X holds
y in M
;
y in A
for
M being
set st
M in Y holds
y in M
then
y in meet Y
by A26, SETFAM_1:def 1;
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;
verum
end; then
A = meet X
by a32, SETFAM_1:def 1;
then
x = Intersect X
by a32, SETFAM_1:def 9;
hence
x in K0
by A29, A31, CANTOR_1:def 3;
verum end; end;
end;
hence
S is SubSpace of T
by TARSKI:2, Th49; verum