set f = X --> y;
set H = the carrier of X;
set HX = [#] X;
let P1 be Subset of REAL ; :: according to PSCOMP_1:def 25 :: thesis: ( not P1 is closed or (X --> y) " P1 is closed )
assume P1 is closed ; :: thesis: (X --> y) " P1 is closed

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:20;
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:22;
hence (X --> y) " P1 is closed ; :: thesis: verum

end;

end;