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

proof

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

now :: thesis: ex y being set st
( y in {X1,X2,X3,X4,X5,X6} & y in Y )

per cases ( Y = X1 or Y = X2 or Y = X3 or Y = X4 or Y = X5 or Y = X6 ) by A8, ENUMSET1:def 4;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

end;

end;

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

end;

X1 in {X1,X2,X3,X4,X5,X6} by ENUMSET1:def 4;
hence contradiction by A7, Th1; :: thesis: verum