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 ) ) )
[#] A c= [#] T by PRE_TOPC:def 9;
then reconsider At = [#] A as Subset of T ;
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 ) )
defpred S₁[ 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 S₁[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 10;
then reconsider FF = F as Subset-Family of (T | AA) ;
for X being Subset of (T | AA) holds
( X in FF iff ex X' being Subset of T st
( X' in G & X' /\ AA = X ) )

proof

let X be Subset of (T | AA); :: thesis: ( X in FF iff ex X' being Subset of T st
( X' in G & X' /\ AA = X ) )
thus ( X in FF implies ex X' being Subset of T st
( X' in G & X' /\ AA = X ) ) :: thesis: ( ex X' being Subset of T st
( X' in G & X' /\ AA = X ) implies X in FF )

proof

assume A4: X in FF ; :: thesis: ex X' being Subset of T st
( X' in G & X' /\ AA = X )
then reconsider XX = X as Subset of A ;
XX is open by A1, A4, Def1;
then consider Y being Subset of T such that
A5: Y is open and
A6: Y /\ ([#] A) = XX by Th32;
take X' = Y; :: thesis: ( X' in G & X' /\ AA = X )
thus ( X' in G & X' /\ AA = X ) by A2, A3, A4, A5, A6; :: thesis: verum

end;

given X' being Subset of T such that A7: ( X' in G & X' /\ AA = X ) ; :: thesis: X in FF
ex X1 being Subset of T st
( X1 = X' & X1 is open & X' /\ At in F ) by A2, A7;
hence X in FF by A3, A7; :: thesis: verum

end;

hence F = G | AA by Def3; :: thesis: verum