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

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