let X, x, Y be set ; :: thesis: (pi X,x) \ (pi Y,x) c= pi (X \ Y),x
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in (pi X,x) \ (pi Y,x) or y in pi (X \ Y),x )
assume A1: y in (pi X,x) \ (pi Y,x) ; :: thesis: y in pi (X \ Y),x
then consider f being Function such that
A2: f in X and
A3: y = f . x by Def6;
not y in pi Y,x by A1, XBOOLE_0:def 5;
then not f in Y by A3, Def6;
then f in X \ Y by A2, XBOOLE_0:def 5;
hence y in pi (X \ Y),x by A3, Def6; :: thesis: verum