let T be TopStruct ; :: thesis: for A being SubSpace of T
for F being Subset-Family of A st F is open holds
ex G being Subset-Family of T st
( G is open & ( for AA being Subset of T st AA = [#] A holds
F = G | AA ) )
let A be SubSpace of T; :: thesis: for F being Subset-Family of A st F is open holds
ex G being Subset-Family of T st
( G is open & ( for AA being Subset of T st AA = [#] A holds
F = G | AA ) )
let F be Subset-Family of A; :: thesis: ( F is open implies ex G being Subset-Family of T st
( G is open & ( for AA being Subset of T st AA = [#] A holds
F = G | AA ) ) )
assume A1: F is open ; :: thesis: ex G being Subset-Family of T st
( G is open & ( for AA being Subset of T st AA = [#] A holds
F = G | AA ) )
[#] A c= [#] T by PRE_TOPC:def 4;
then reconsider At = [#] A as Subset of T ;
defpred S1[ Subset of T] means ex X1 being Subset of T st
( X1 = $1 & X1 is open & $1 /\ At in F );
consider G being Subset-Family of T such that
A2: for X being Subset of T holds
( X in G iff S1[X] ) from SUBSET_1:sch 3();
 take G ; :: thesis: ( G is open & ( for AA being Subset of T st AA = [#] A holds
F = G | AA ) )
thus G is open :: thesis: for AA being Subset of T st AA = [#] A holds
F = G | AA
proof
let H be Subset of T; :: according to TOPS_2:def 1 :: thesis: ( H in G implies H is open )
assume H in G ; :: thesis: H is open
then ex X1 being Subset of T st
( X1 = H & X1 is open & H /\ At in F ) by A2;
hence H is open ; :: thesis: verum
end;
let AA be Subset of T; :: thesis: ( AA = [#] A implies F = G | AA )
assume A3: AA = [#] A ; :: thesis: F = G | AA
then F c= bool AA ;
then F c= bool ([#] (T | AA)) by PRE_TOPC:def 5;
then reconsider FF = F as Subset-Family of (T | AA) ;
for X being Subset of (T | AA) holds
( X in FF iff ex X9 being Subset of T st
( X9 in G & X9 /\ AA = X ) )
proof
let X be Subset of (T | AA); :: thesis: ( X in FF iff ex X9 being Subset of T st
( X9 in G & X9 /\ AA = X ) )
thus ( X in FF implies ex X9 being Subset of T st
( X9 in G & X9 /\ AA = X ) ) :: thesis: ( ex X9 being Subset of T st
( X9 in G & X9 /\ AA = X ) implies X in FF )
proof
assume A4: X in FF ; :: thesis: ex X9 being Subset of T st
( X9 in G & X9 /\ AA = X )
then reconsider XX = X as Subset of A ;
XX is open by A1, A4;
then consider Y being Subset of T such that
A5: ( Y is open & Y /\ ([#] A) = XX ) by Th24;
take Y ; :: thesis: ( Y in G & Y /\ AA = X )
thus ( Y in G & Y /\ AA = X ) by A2, A3, A4, A5; :: thesis: verum
end;
given X9 being Subset of T such that A6: X9 in G and
A7: X9 /\ AA = X ; :: thesis: X in FF
ex X1 being Subset of T st
( X1 = X9 & X1 is open & X9 /\ At in F ) by A2, A6;
hence X in FF by A3, A7; :: thesis: verum
end;
hence F = G | AA by Def3; :: thesis: verum