let A, B be set ; :: thesis: for x being object st A = B \ {x} & x in B holds
B \ A = {x}
let x be object ; :: thesis: ( A = B \ {x} & x in B implies B \ A = {x} )
assume that
A1: A = B \ {x} and
A2: x in B ; :: thesis: B \ A = {x}
reconsider A = A as Subset of B by A1;
reconsider iks = {x} as Subset of B by A2, ZFMISC_1:31;
A = iks ` by A1, SUBSET_1:def 4;
then A ` = iks ;
hence B \ A = {x} by SUBSET_1:def 4; :: thesis: verum