let X, Y be non empty TopSpace; :: thesis: for f being Function of X,Y holds
( f is continuous iff ( f is p-continuous & f is (c,p)-continuous ) )
let f be Function of X,Y; :: thesis: ( f is continuous iff ( f is p-continuous & f is (c,p)-continuous ) )
A1: [#] Y <> {} ;

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

assume A2: f is continuous ; :: thesis: ( f is p-continuous & f is (c,p)-continuous )
thus f is p-continuous :: thesis: f is (c,p)-continuous

proof

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 is open by A1, A2, TOPS_2:43;
then f " V in the topology of X by PRE_TOPC:def 2;
then f " V in (PO X) /\ (D(c,p) X) by Th9;
hence f " V in PO X by XBOOLE_0:def 4; :: thesis: verum

end;

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

proof

let V be Subset of Y; :: according to DECOMP_1:def 33 :: thesis: ( V is open implies f " V in D(c,p) X )
assume V is open ; :: thesis: f " V in D(c,p) X
then f " V is open by A1, A2, TOPS_2:43;
then f " V in the topology of X by PRE_TOPC:def 2;
then f " V in (PO X) /\ (D(c,p) X) by Th9;
hence f " V in D(c,p) X by XBOOLE_0:def 4; :: thesis: verum

end;

end;

assume A3: ( f is p-continuous & f is (c,p)-continuous ) ; :: thesis: f is continuous

now :: thesis: for V being Subset of Y st V is open holds
f " V is open

let V be Subset of Y; :: thesis: ( V is open implies f " V is open )
assume V is open ; :: thesis: f " V is open
then ( f " V in PO X & f " V in D(c,p) X ) by A3;
then f " V in (PO X) /\ (D(c,p) X) by XBOOLE_0:def 4;
then f " V in the topology of X by Th9;
hence f " V is open by PRE_TOPC:def 2; :: thesis: verum

end;

hence f is continuous by A1, TOPS_2:43; :: thesis: verum