set f = X --> y;
set HX = [#] X;
let P1 be Subset of REAL; :: according to PSCOMP_1:def 3 :: 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: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;