let x, y, z be set ; ( x <> y & x <> z implies {x,y,z} \ {x} = {y,z} )
assume A1:
( x <> y & x <> z )
; {x,y,z} \ {x} = {y,z}
hereby TARSKI:def 3,
XBOOLE_0:def 10 {y,z} c= {x,y,z} \ {x}
let a be
object ;
( a in {x,y,z} \ {x} implies a in {y,z} )assume A2:
a in {x,y,z} \ {x}
;
a in {y,z}then
a in {x,y,z}
by XBOOLE_0:def 5;
then A3:
(
a = x or
a = y or
a = z )
by Def1;
not
a in {x}
by A2, XBOOLE_0:def 5;
hence
a in {y,z}
by A3, TARSKI:def 1, TARSKI:def 2;
verum
end;
let a be object ; TARSKI:def 3 ( not a in {y,z} or a in {x,y,z} \ {x} )
assume
a in {y,z}
; a in {x,y,z} \ {x}
then A4:
( a = y or a = z )
by TARSKI:def 2;
then A5:
not a in {x}
by A1, TARSKI:def 1;
a in {x,y,z}
by A4, Def1;
hence
a in {x,y,z} \ {x}
by A5, XBOOLE_0:def 5; verum