let X1, X2, X3, X4, X5, X6, X7, X8 be set ; :: thesis: ( not X1 in X2 or not X2 in X3 or not X3 in X4 or not X4 in X5 or not X5 in X6 or not X6 in X7 or not X7 in X8 or not X8 in X1 )
assume that
A1: X1 in X2 and
A2: X2 in X3 and
A3: X3 in X4 and
A4: X4 in X5 and
A5: X5 in X6 and
A6: X6 in X7 and
A7: X7 in X8 and
A8: X8 in X1 ; :: thesis: contradiction
set Z = {X1,X2,X3,X4,X5,X6,X7,X8};
for Y being set st Y in {X1,X2,X3,X4,X5,X6,X7,X8} holds
{X1,X2,X3,X4,X5,X6,X7,X8} meets Y
proof
let Y be set ; :: thesis: ( Y in {X1,X2,X3,X4,X5,X6,X7,X8} implies {X1,X2,X3,X4,X5,X6,X7,X8} meets Y )
assume A10: Y in {X1,X2,X3,X4,X5,X6,X7,X8} ; :: thesis: {X1,X2,X3,X4,X5,X6,X7,X8} meets Y
now :: thesis: ex y being set st
( y in {X1,X2,X3,X4,X5,X6,X7,X8} & y in Y )
per cases ( Y = X1 or Y = X2 or Y = X3 or Y = X4 or Y = X5 or Y = X6 or Y = X7 or Y = X8 ) by A10, ENUMSET1:def 6;
suppose A11: Y = X1 ; :: thesis: ex y being set st
( y in {X1,X2,X3,X4,X5,X6,X7,X8} & y in Y )
take y = X8; :: thesis: ( y in {X1,X2,X3,X4,X5,X6,X7,X8} & y in Y )
thus ( y in {X1,X2,X3,X4,X5,X6,X7,X8} & y in Y ) by A8, A11, ENUMSET1:def 6; :: thesis: verum
end;
suppose A12: Y = X2 ; :: thesis: ex y being set st
( y in {X1,X2,X3,X4,X5,X6,X7,X8} & y in Y )
take y = X1; :: thesis: ( y in {X1,X2,X3,X4,X5,X6,X7,X8} & y in Y )
thus ( y in {X1,X2,X3,X4,X5,X6,X7,X8} & y in Y ) by A1, A12, ENUMSET1:def 6; :: thesis: verum
end;
suppose A13: Y = X3 ; :: thesis: ex y being set st
( y in {X1,X2,X3,X4,X5,X6,X7,X8} & y in Y )
take y = X2; :: thesis: ( y in {X1,X2,X3,X4,X5,X6,X7,X8} & y in Y )
thus ( y in {X1,X2,X3,X4,X5,X6,X7,X8} & y in Y ) by A2, A13, ENUMSET1:def 6; :: thesis: verum
end;
suppose A14: Y = X4 ; :: thesis: ex y being set st
( y in {X1,X2,X3,X4,X5,X6,X7,X8} & y in Y )
take y = X3; :: thesis: ( y in {X1,X2,X3,X4,X5,X6,X7,X8} & y in Y )
thus ( y in {X1,X2,X3,X4,X5,X6,X7,X8} & y in Y ) by A3, A14, ENUMSET1:def 6; :: thesis: verum
end;
suppose A15: Y = X5 ; :: thesis: ex y being set st
( y in {X1,X2,X3,X4,X5,X6,X7,X8} & y in Y )
take y = X4; :: thesis: ( y in {X1,X2,X3,X4,X5,X6,X7,X8} & y in Y )
thus ( y in {X1,X2,X3,X4,X5,X6,X7,X8} & y in Y ) by A4, A15, ENUMSET1:def 6; :: thesis: verum
end;
suppose A16: Y = X6 ; :: thesis: ex y being set st
( y in {X1,X2,X3,X4,X5,X6,X7,X8} & y in Y )
take y = X5; :: thesis: ( y in {X1,X2,X3,X4,X5,X6,X7,X8} & y in Y )
thus ( y in {X1,X2,X3,X4,X5,X6,X7,X8} & y in Y ) by A5, A16, ENUMSET1:def 6; :: thesis: verum
end;
suppose A17: Y = X7 ; :: thesis: ex y being set st
( y in {X1,X2,X3,X4,X5,X6,X7,X8} & y in Y )
take y = X6; :: thesis: ( y in {X1,X2,X3,X4,X5,X6,X7,X8} & y in Y )
thus ( y in {X1,X2,X3,X4,X5,X6,X7,X8} & y in Y ) by A6, A17, ENUMSET1:def 6; :: thesis: verum
end;
suppose A18: Y = X8 ; :: thesis: ex y being set st
( y in {X1,X2,X3,X4,X5,X6,X7,X8} & y in Y )
take y = X7; :: thesis: ( y in {X1,X2,X3,X4,X5,X6,X7,X8} & y in Y )
thus ( y in {X1,X2,X3,X4,X5,X6,X7,X8} & y in Y ) by A7, A18, ENUMSET1:def 6; :: thesis: verum
end;
end;
end;
hence {X1,X2,X3,X4,X5,X6,X7,X8} meets Y by XBOOLE_0:3; :: thesis: verum
end;
hence contradiction by XREGULAR:1; :: thesis: verum