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)
A1: (pi (X,x)) \ (pi (Y,x)) c= pi ((X \ Y),x) by Th18;
A2: (pi (Y,x)) \ (pi (X,x)) c= pi ((Y \ X),x) by Th18;
(pi ((X \ Y),x)) \/ (pi ((Y \ X),x)) = pi (((X \ Y) \/ (Y \ X)),x) by Th16;
hence (pi (X,x)) \+\ (pi (Y,x)) c= pi ((X \+\ Y),x) by A1, A2, XBOOLE_1:13; :: thesis: verum