let X, Y be set ; :: thesis: for t, s, z being object st X c= Y & t in Y & s in Y & z in Y holds
(X \ {t,s}) \/ {z} c= Y
let t, s, z be object ; :: thesis: ( X c= Y & t in Y & s in Y & z in Y implies (X \ {t,s}) \/ {z} c= Y )
assume A1: ( X c= Y & t in Y & s in Y & z in Y ) ; :: thesis: (X \ {t,s}) \/ {z} c= Y
A2: X \ {t,s} c= Y by A1, XBOOLE_1:1;
{z} c= Y by ZFMISC_1:31, A1;
hence (X \ {t,s}) \/ {z} c= Y by A2, XBOOLE_1:8; :: thesis: verum