let X, x, Y be set ; :: thesis: (pi X,x) \+\ (pi Y,x) c= pi (X \+\ Y),x
A1: (pi X,x) \ (pi Y,x) c= pi (X \ Y),x by Th29;
A2: (pi Y,x) \ (pi X,x) c= pi (Y \ X),x by Th29;
(pi (X \ Y),x) \/ (pi (Y \ X),x) = pi ((X \ Y) \/ (Y \ X)),x by Th27;
hence (pi X,x) \+\ (pi Y,x) c= pi (X \+\ Y),x by A1, A2, XBOOLE_1:13; :: thesis: verum