let x be object ; :: thesis: for X, Y being set holds (pi (X,x)) \ (pi (Y,x)) c= pi ((X \ Y),x)
let X, Y be set ; :: thesis: (pi (X,x)) \ (pi (Y,x)) c= pi ((X \ Y),x)
let y be object ; :: 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