let F be finite set ; :: thesis: for A being FinSequence of bool F
for i being Element of NAT
for x, y being set st x <> y & x in A . i & y in A . i holds
((A . i) \ {x}) \/ ((A . i) \ {y}) = A . i
let A be FinSequence of bool F; :: thesis: for i being Element of NAT
for x, y being set st x <> y & x in A . i & y in A . i holds
((A . i) \ {x}) \/ ((A . i) \ {y}) = A . i
let i be Element of NAT ; :: thesis: for x, y being set st x <> y & x in A . i & y in A . i holds
((A . i) \ {x}) \/ ((A . i) \ {y}) = A . i
let x, y be set ; :: thesis: ( x <> y & x in A . i & y in A . i implies ((A . i) \ {x}) \/ ((A . i) \ {y}) = A . i )
assume that
A1: x <> y and
A2: x in A . i and
A3: y in A . i ; :: thesis: ((A . i) \ {x}) \/ ((A . i) \ {y}) = A . i
((A . i) \ {x}) \/ ((A . i) \ {y}) = A . i

proof

thus ((A . i) \ {x}) \/ ((A . i) \ {y}) c= A . i ; :: according to XBOOLE_0:def 10 :: thesis: A . i c= ((A . i) \ {x}) \/ ((A . i) \ {y})
thus A . i c= ((A . i) \ {x}) \/ ((A . i) \ {y}) :: thesis: verum

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in A . i or z in ((A . i) \ {x}) \/ ((A . i) \ {y}) )
assume A4: z in A . i ; :: thesis: z in ((A . i) \ {x}) \/ ((A . i) \ {y})
{} = {y} \ ({y} \/ {} ) by XBOOLE_1:46;
then A . i = (A . i) \ ({y} \ {y}) ;
then A . i = ((A . i) \ {y}) \/ ((A . i) /\ {y}) by XBOOLE_1:52;
then A5: A . i = ((A . i) \ {y}) \/ {y} by A3, ZFMISC_1:52;
not x in {y} by A1, TARSKI:def 1;
then A6: x in (A . i) \ {y} by A2, XBOOLE_0:def 5;
not y in {x} by A1, TARSKI:def 1;
then A7: y in (A . i) \ {x} by A3, XBOOLE_0:def 5;
z in (((A . i) \ {x}) \/ {x}) \/ (((A . i) \ {y}) \/ {y}) by A4, A5, XBOOLE_0:def 3;
then z in ((A . i) \ {x}) \/ ({x} \/ ({y} \/ ((A . i) \ {y}))) by XBOOLE_1:4;
then z in ((A . i) \ {x}) \/ (({x} \/ {y}) \/ ((A . i) \ {y})) by XBOOLE_1:4;
then z in (((A . i) \ {x}) \/ ({y} \/ {x})) \/ ((A . i) \ {y}) by XBOOLE_1:4;
then z in ((((A . i) \ {x}) \/ {y}) \/ {x}) \/ ((A . i) \ {y}) by XBOOLE_1:4;
then z in (((A . i) \ {x}) \/ {y}) \/ ({x} \/ ((A . i) \ {y})) by XBOOLE_1:4;
then z in ((A . i) \ {x}) \/ ({x} \/ ((A . i) \ {y})) by A7, ZFMISC_1:46;
hence z in ((A . i) \ {x}) \/ ((A . i) \ {y}) by A6, ZFMISC_1:46; :: thesis: verum

end;

end;

hence ((A . i) \ {x}) \/ ((A . i) \ {y}) = A . i ; :: thesis: verum