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 A3, CANTOR_1:def 3;
per cases ( X <> {} or X = {} ) ;
suppose A5: X <> {} ; :: thesis: 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] )
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 A2, A4, SETFAM_1:def 5;
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 A8, TARSKI:def 1; :: 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 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) )
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 A6, A9, A14, A15, SETFAM_1:def 1;
hence y in D by A16, TARSKI:def 3, XBOOLE_1:17; :: thesis: verum
end;
then A17: y in meet Y by A12, SETFAM_1:def 1;
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;
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 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;
hence y in A by A5, A6, SETFAM_1:def 1; :: 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 A13, A21, SETFAM_1:def 5; :: thesis: verum
end;
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 )
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 A1, A22, XBOOLE_1:28, TARSKI:def 1, A23, CANTOR_1:def 3; :: 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 A24, CANTOR_1:def 3;
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 A2, A25, A28, SETFAM_1:def 5; :: 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 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 ; :: 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 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;
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 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;
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; :: thesis: 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; :: thesis: verum
end;
end;
end;
hence S is SubSpace of T by TARSKI:2, Th49; :: thesis: verum