let X1, X2, X3, X4, X5, X6, X7 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 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 X1 ; :: thesis: contradiction
set Z = {X1,X2,X3,X4,X5,X6,X7};
for Y being set st Y in {X1,X2,X3,X4,X5,X6,X7} holds
{X1,X2,X3,X4,X5,X6,X7} meets Y

proof

let Y be set ; :: thesis: ( Y in {X1,X2,X3,X4,X5,X6,X7} implies {X1,X2,X3,X4,X5,X6,X7} meets Y )
assume A9: Y in {X1,X2,X3,X4,X5,X6,X7} ; :: thesis: {X1,X2,X3,X4,X5,X6,X7} meets Y

now :: thesis: ex y being set st
( y in {X1,X2,X3,X4,X5,X6,X7} & 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 ) by A9, ENUMSET1:def 5;

suppose A10: Y = X1 ; :: thesis: ex y being set st
( y in {X1,X2,X3,X4,X5,X6,X7} & y in Y )

take y = X7; :: thesis: ( y in {X1,X2,X3,X4,X5,X6,X7} & y in Y )
thus ( y in {X1,X2,X3,X4,X5,X6,X7} & y in Y ) by A7, A10, ENUMSET1:def 5; :: thesis: verum

end;

suppose A11: Y = X2 ; :: thesis: ex y being set st
( y in {X1,X2,X3,X4,X5,X6,X7} & y in Y )

take y = X1; :: thesis: ( y in {X1,X2,X3,X4,X5,X6,X7} & y in Y )
thus ( y in {X1,X2,X3,X4,X5,X6,X7} & y in Y ) by A1, A11, ENUMSET1:def 5; :: thesis: verum

end;

suppose A12: Y = X3 ; :: thesis: ex y being set st
( y in {X1,X2,X3,X4,X5,X6,X7} & y in Y )

take y = X2; :: thesis: ( y in {X1,X2,X3,X4,X5,X6,X7} & y in Y )
thus ( y in {X1,X2,X3,X4,X5,X6,X7} & y in Y ) by A2, A12, ENUMSET1:def 5; :: thesis: verum

end;

suppose A13: Y = X4 ; :: thesis: ex y being set st
( y in {X1,X2,X3,X4,X5,X6,X7} & y in Y )

take y = X3; :: thesis: ( y in {X1,X2,X3,X4,X5,X6,X7} & y in Y )
thus ( y in {X1,X2,X3,X4,X5,X6,X7} & y in Y ) by A3, A13, ENUMSET1:def 5; :: thesis: verum

end;

suppose A14: Y = X5 ; :: thesis: ex y being set st
( y in {X1,X2,X3,X4,X5,X6,X7} & y in Y )

take y = X4; :: thesis: ( y in {X1,X2,X3,X4,X5,X6,X7} & y in Y )
thus ( y in {X1,X2,X3,X4,X5,X6,X7} & y in Y ) by A4, A14, ENUMSET1:def 5; :: thesis: verum

end;

suppose A15: Y = X6 ; :: thesis: ex y being set st
( y in {X1,X2,X3,X4,X5,X6,X7} & y in Y )

take y = X5; :: thesis: ( y in {X1,X2,X3,X4,X5,X6,X7} & y in Y )
thus ( y in {X1,X2,X3,X4,X5,X6,X7} & y in Y ) by A5, A15, ENUMSET1:def 5; :: thesis: verum

end;

suppose A16: Y = X7 ; :: thesis: ex y being set st
( y in {X1,X2,X3,X4,X5,X6,X7} & y in Y )

take y = X6; :: thesis: ( y in {X1,X2,X3,X4,X5,X6,X7} & y in Y )
thus ( y in {X1,X2,X3,X4,X5,X6,X7} & y in Y ) by A6, A16, ENUMSET1:def 5; :: thesis: verum

end;

end;

end;

hence {X1,X2,X3,X4,X5,X6,X7} meets Y by XBOOLE_0:3; :: thesis: verum

end;

hence contradiction by XREGULAR:1; :: thesis: verum