let X be finite set ; :: thesis: for t, s, z being object st t in X & s in X & t <> s & not z in X holds
card ((X \ {t,s}) \/ {z}) = (card X) - 1
let t, s, z be object ; :: thesis: ( t in X & s in X & t <> s & not z in X implies card ((X \ {t,s}) \/ {z}) = (card X) - 1 )
assume A1: ( t in X & s in X & t <> s & not z in X ) ; :: thesis: card ((X \ {t,s}) \/ {z}) = (card X) - 1
A2: X = (X \ {t,s}) \/ {t,s} by XBOOLE_1:45, ZFMISC_1:32, A1;
A3: card X = (card (X \ {t,s})) + (card {t,s}) by XBOOLE_1:79, A2, CARD_2:40
.= (card (X \ {t,s})) + 2 by CARD_2:57, A1 ;
X misses {z} by A1, ZFMISC_1:50;
hence card ((X \ {t,s}) \/ {z}) = (card (X \ {t,s})) + (card {z}) by CARD_2:40, XBOOLE_1:63
.= ((card X) - 2) + 1 by CARD_1:30, A3
.= (card X) - 1 ;
:: thesis: verum