let x1, x2, x3, x4, x5, x6 be set ; {x1,x2,x3,x4,x5,x6} = {x1,x3,x6} \/ {x2,x4,x5}
thus
{x1,x2,x3,x4,x5,x6} c= {x1,x3,x6} \/ {x2,x4,x5}
XBOOLE_0:def 10 {x1,x3,x6} \/ {x2,x4,x5} c= {x1,x2,x3,x4,x5,x6}proof
let x be
object ;
TARSKI:def 3 ( not x in {x1,x2,x3,x4,x5,x6} or x in {x1,x3,x6} \/ {x2,x4,x5} )
assume
x in {x1,x2,x3,x4,x5,x6}
;
x in {x1,x3,x6} \/ {x2,x4,x5}
then
(
x = x1 or
x = x2 or
x = x3 or
x = x4 or
x = x5 or
x = x6 )
by ENUMSET1:def 4;
then
(
x in {x1,x3,x6} or
x in {x2,x4,x5} )
by ENUMSET1:def 1;
hence
x in {x1,x3,x6} \/ {x2,x4,x5}
by XBOOLE_0:def 3;
verum
end;
let x be object ; TARSKI:def 3 ( not x in {x1,x3,x6} \/ {x2,x4,x5} or x in {x1,x2,x3,x4,x5,x6} )
assume
x in {x1,x3,x6} \/ {x2,x4,x5}
; x in {x1,x2,x3,x4,x5,x6}
then
( x in {x1,x3,x6} or x in {x2,x4,x5} )
by XBOOLE_0:def 3;
then
( x = x1 or x = x3 or x = x6 or x = x2 or x = x4 or x = x5 )
by ENUMSET1:def 1;
hence
x in {x1,x2,x3,x4,x5,x6}
by ENUMSET1:def 4; verum