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 set ; :: according to TARSKI:def 3 :: thesis: ( not a in {x,y,z} or a in Z )
assume A9: a in {x,y,z} ; :: thesis: a in Z

A10: now

assume not x in Z ; :: thesis: contradiction
then A11: Z c= {x,y,z} \ {x} by A1, Lm2;
{x,y,z} \ {x} = ({x} \/ {y,z}) \ {x} by ENUMSET1:42
.= {y,z} \ {x} by XBOOLE_1:40 ;
then {x,y,z} \ {x} c= {y,z} by XBOOLE_1:36;
then Z c= {y,z} by A11, XBOOLE_1:1;
hence contradiction by A2, A4, A5, A7, Lm14; :: thesis: verum

end;

A12: now

assume not y in Z ; :: thesis: contradiction
then A13: Z c= {x,y,z} \ {y} by A1, Lm2;
{x,y,z} \ {y} = ({x,y} \/ {z}) \ {y} by ENUMSET1:43
.= (({x} \/ {y}) \/ {z}) \ {y} by ENUMSET1:41
.= (({x} \/ {z}) \/ {y}) \ {y} by XBOOLE_1:4
.= ({x,z} \/ {y}) \ {y} by ENUMSET1:41
.= {x,z} \ {y} by XBOOLE_1:40 ;
then {x,y,z} \ {y} c= {x,z} by XBOOLE_1:36;
then Z c= {x,z} by A13, XBOOLE_1:1;
hence contradiction by A2, A3, A5, A8, Lm14; :: thesis: verum

end;

now

assume not z in Z ; :: thesis: contradiction
then A14: Z c= {x,y,z} \ {z} by A1, Lm2;
{x,y,z} \ {z} = ({x,y} \/ {z}) \ {z} by ENUMSET1:43
.= {x,y} \ {z} by XBOOLE_1:40 ;
then {x,y,z} \ {z} c= {x,y} by XBOOLE_1:36;
then Z c= {x,y} by A14, XBOOLE_1:1;
hence contradiction by A2, A3, A4, A6, Lm14; :: thesis: verum

end;

hence a in Z by A9, A10, A12, ENUMSET1:def 1; :: thesis: verum

end;

hence Z = {x,y,z} by A1, XBOOLE_0:def 10; :: 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} by XBOOLE_1:2; :: 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:42; :: thesis: verum

end;

suppose Z = {y} ; :: thesis: Z c= {x,y,z}

then A16: Z c= {x,y} by Th12;
{x,y} c= {x,y} \/ {z} by XBOOLE_1:7;
then {x,y} c= {x,y,z} by ENUMSET1:43;
hence Z c= {x,y,z} by A16, XBOOLE_1:1; :: 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:43; :: 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:43; :: 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:42; :: thesis: verum

end;

suppose Z = {x,z} ; :: thesis: Z c= {x,y,z}

then A17: Z c= {x,z} \/ {y} by XBOOLE_1:7;
{x,z} \/ {y} = ({x} \/ {z}) \/ {y} by ENUMSET1:41
.= {x} \/ ({y} \/ {z}) by XBOOLE_1:4
.= {x} \/ {y,z} by ENUMSET1:41 ;
hence Z c= {x,y,z} by A17, ENUMSET1:42; :: thesis: verum

end;

suppose Z = {x,y,z} ; :: thesis: Z c= {x,y,z}

hence Z c= {x,y,z} ; :: thesis: verum

end;

end;