let X, Y be non empty TopSpace; :: thesis: for f being Function of X,Y holds
( f is p-continuous iff ( f is sp-continuous & f is (p,sp)-continuous ) )
let f be Function of X,Y; :: thesis: ( f is p-continuous iff ( f is sp-continuous & f is (p,sp)-continuous ) )

hereby :: thesis: ( f is sp-continuous & f is (p,sp)-continuous implies f is p-continuous )

assume A1: f is p-continuous ; :: thesis: ( f is sp-continuous & f is (p,sp)-continuous )
thus f is sp-continuous :: thesis: f is (p,sp)-continuous

proof

let V be Subset of Y; :: according to DECOMP_1:def 30 :: thesis: ( V is open implies f " V in SPO X )
assume V is open ; :: thesis: f " V in SPO X
then f " V in PO X by A1;
then f " V in (SPO X) /\ (D(p,sp) X) by Th14;
hence f " V in SPO X by XBOOLE_0:def 4; :: thesis: verum

end;

thus f is (p,sp)-continuous :: thesis: verum

proof

let G be Subset of Y; :: according to DECOMP_1:def 39 :: thesis: ( G is open implies f " G in D(p,sp) X )
assume G is open ; :: thesis: f " G in D(p,sp) X
then f " G in PO X by A1;
then f " G in (SPO X) /\ (D(p,sp) X) by Th14;
hence f " G in D(p,sp) X by XBOOLE_0:def 4; :: thesis: verum

end;

end;

assume A2: ( f is sp-continuous & f is (p,sp)-continuous ) ; :: thesis: f is p-continuous
let V be Subset of Y; :: according to DECOMP_1:def 27 :: thesis: ( V is open implies f " V in PO X )
assume V is open ; :: thesis: f " V in PO X
then ( f " V in SPO X & f " V in D(p,sp) X ) by A2;
then f " V in (SPO X) /\ (D(p,sp) X) by XBOOLE_0:def 4;
hence f " V in PO X by Th14; :: thesis: verum