let X1, X2, X3, X4, X5 be set ; ( not X1 in X2 or not X2 in X3 or not X3 in X4 or not X4 in X5 or not X5 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 X1
; contradiction
set Z = {X1,X2,X3,X4,X5};
A6:
for Y being set st Y in {X1,X2,X3,X4,X5} holds
{X1,X2,X3,X4,X5} meets Y
proof
let Y be
set ;
( Y in {X1,X2,X3,X4,X5} implies {X1,X2,X3,X4,X5} meets Y )
assume A7:
Y in {X1,X2,X3,X4,X5}
;
{X1,X2,X3,X4,X5} meets Y
now ex y being set st
( y in {X1,X2,X3,X4,X5} & y in Y )per cases
( Y = X1 or Y = X2 or Y = X3 or Y = X4 or Y = X5 )
by A7, ENUMSET1:def 3;
suppose A8:
Y = X1
;
ex y being set st
( y in {X1,X2,X3,X4,X5} & y in Y )take y =
X5;
( y in {X1,X2,X3,X4,X5} & y in Y )thus
(
y in {X1,X2,X3,X4,X5} &
y in Y )
by A5, A8, ENUMSET1:def 3;
verum end; suppose A9:
Y = X2
;
ex y being set st
( y in {X1,X2,X3,X4,X5} & y in Y )take y =
X1;
( y in {X1,X2,X3,X4,X5} & y in Y )thus
(
y in {X1,X2,X3,X4,X5} &
y in Y )
by A1, A9, ENUMSET1:def 3;
verum end; suppose A10:
Y = X3
;
ex y being set st
( y in {X1,X2,X3,X4,X5} & y in Y )take y =
X2;
( y in {X1,X2,X3,X4,X5} & y in Y )thus
(
y in {X1,X2,X3,X4,X5} &
y in Y )
by A2, A10, ENUMSET1:def 3;
verum end; suppose A11:
Y = X4
;
ex y being set st
( y in {X1,X2,X3,X4,X5} & y in Y )take y =
X3;
( y in {X1,X2,X3,X4,X5} & y in Y )thus
(
y in {X1,X2,X3,X4,X5} &
y in Y )
by A3, A11, ENUMSET1:def 3;
verum end; suppose A12:
Y = X5
;
ex y being set st
( y in {X1,X2,X3,X4,X5} & y in Y )take y =
X4;
( y in {X1,X2,X3,X4,X5} & y in Y )thus
(
y in {X1,X2,X3,X4,X5} &
y in Y )
by A4, A12, ENUMSET1:def 3;
verum end;
hence
{X1,X2,X3,X4,X5} meets Y
by XBOOLE_0:3;
verum
end;
X1 in {X1,X2,X3,X4,X5}
by ENUMSET1:def 3;
hence
contradiction
by A6, Th1; verum