let x, y, z, Z be set ; :: thesis: ( Z c= {x,y,z} iff ( Z = {} or Z = {x} or Z = {y} or Z = {z} or Z = {x,y} or Z = {y,z} or Z = {x,z} or Z = {x,y,z} ) )
hereby :: thesis: ( ( Z = {} or Z = {x} or Z = {y} or Z = {z} or Z = {x,y} or Z = {y,z} or Z = {x,z} or Z = {x,y,z} ) implies Z c= {x,y,z} )
assume that
A1: Z c= {x,y,z} and
A2: Z <> {} and
A3: Z <> {x} and
A4: Z <> {y} and
A5: Z <> {z} and
A6: Z <> {x,y} and
A7: Z <> {y,z} and
A8: Z <> {x,z} ; :: thesis: Z = {x,y,z}
{x,y,z} c= Z
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in {x,y,z} or a in Z )
A9: now :: thesis: x in Z
{x,y,z} \ {x} = ({x} \/ {y,z}) \ {x} by ENUMSET1:2
.= {y,z} \ {x} by XBOOLE_1:40 ;
then A10: {x,y,z} \ {x} c= {y,z} by XBOOLE_1:36;
assume not x in Z ; :: thesis: contradiction
then Z c= {x,y,z} \ {x} by A1, Lm2;
hence contradiction by A2, A4, A5, A7, Lm13, A10, XBOOLE_1:1; :: thesis: verum
end;
A11: now :: thesis: y in Z
{x,y,z} \ {y} = ({x,y} \/ {z}) \ {y} by ENUMSET1:3
.= (({x} \/ {y}) \/ {z}) \ {y} by ENUMSET1:1
.= (({x} \/ {z}) \/ {y}) \ {y} by XBOOLE_1:4
.= ({x,z} \/ {y}) \ {y} by ENUMSET1:1
.= {x,z} \ {y} by XBOOLE_1:40 ;
then A12: {x,y,z} \ {y} c= {x,z} by XBOOLE_1:36;
assume not y in Z ; :: thesis: contradiction
then Z c= {x,y,z} \ {y} by A1, Lm2;
hence contradiction by A2, A3, A5, A8, Lm13, A12, XBOOLE_1:1; :: thesis: verum
end;
A13: now :: thesis: z in Z
{x,y,z} \ {z} = ({x,y} \/ {z}) \ {z} by ENUMSET1:3
.= {x,y} \ {z} by XBOOLE_1:40 ;
then A14: {x,y,z} \ {z} c= {x,y} by XBOOLE_1:36;
assume not z in Z ; :: thesis: contradiction
then Z c= {x,y,z} \ {z} by A1, Lm2;
hence contradiction by A2, A3, A4, A6, Lm13, A14, XBOOLE_1:1; :: thesis: verum
end;
assume a in {x,y,z} ; :: thesis: a in Z
hence a in Z by A9, A11, A13, ENUMSET1:def 1; :: thesis: verum
end;
hence Z = {x,y,z} by A1; :: thesis: verum
end;
assume A15: ( Z = {} or Z = {x} or Z = {y} or Z = {z} or Z = {x,y} or Z = {y,z} or Z = {x,z} or Z = {x,y,z} ) ; :: thesis: Z c= {x,y,z}
per cases ( Z = {} or Z = {x} or Z = {y} or Z = {z} or Z = {x,y} or Z = {y,z} or Z = {x,z} or Z = {x,y,z} ) by A15;
suppose Z = {} ; :: thesis: Z c= {x,y,z}
hence Z c= {x,y,z} ; :: thesis: verum
end;
suppose Z = {x} ; :: thesis: Z c= {x,y,z}
then Z c= {x} \/ {y,z} by XBOOLE_1:7;
hence Z c= {x,y,z} by ENUMSET1:2; :: thesis: verum
end;
suppose A16: Z = {y} ; :: thesis: Z c= {x,y,z}
{x,y} c= {x,y} \/ {z} by XBOOLE_1:7;
then A17: {x,y} c= {x,y,z} by ENUMSET1:3;
Z c= {x,y} by A16, Th7;
hence Z c= {x,y,z} by A17; :: thesis: verum
end;
suppose Z = {z} ; :: thesis: Z c= {x,y,z}
then Z c= {x,y} \/ {z} by XBOOLE_1:7;
hence Z c= {x,y,z} by ENUMSET1:3; :: thesis: verum
end;
suppose Z = {x,y} ; :: thesis: Z c= {x,y,z}
then Z c= {x,y} \/ {z} by XBOOLE_1:7;
hence Z c= {x,y,z} by ENUMSET1:3; :: thesis: verum
end;
suppose Z = {y,z} ; :: thesis: Z c= {x,y,z}
then Z c= {x} \/ {y,z} by XBOOLE_1:7;
hence Z c= {x,y,z} by ENUMSET1:2; :: thesis: verum
end;
suppose A18: Z = {x,z} ; :: thesis: Z c= {x,y,z}
A19: {x,z} \/ {y} = ({x} \/ {z}) \/ {y} by ENUMSET1:1
.= {x} \/ ({y} \/ {z}) by XBOOLE_1:4
.= {x} \/ {y,z} by ENUMSET1:1 ;
Z c= {x,z} \/ {y} by A18, XBOOLE_1:7;
hence Z c= {x,y,z} by A19, ENUMSET1:2; :: thesis: verum
end;
suppose Z = {x,y,z} ; :: thesis: Z c= {x,y,z}
hence Z c= {x,y,z} ; :: thesis: verum
end;
end;