let P1 be Subset of Y; :: according to PRE_TOPC:def 6 :: thesis: ( P1 is closed implies (X --> y) " P1 is closed )
assume P1 is closed ; :: thesis: (X --> y) " P1 is closed
set F = X --> y;
set H = [#] X;

per cases ( y in P1 or not y in P1 ) ;

suppose y in P1 ; :: thesis: (X --> y) " P1 is closed

then (X --> y) " P1 = [#] X by FUNCOP_1:14;
hence (X --> y) " P1 is closed ; :: thesis: verum

end;

suppose not y in P1 ; :: thesis: (X --> y) " P1 is closed

then (X --> y) " P1 = {} X by FUNCOP_1:16;
hence (X --> y) " P1 is closed ; :: thesis: verum

end;

end;