let X1, X2, X3, X4, X5 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 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 ; :: thesis: 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 ; :: thesis: ( Y in {X1,X2,X3,X4,X5} implies {X1,X2,X3,X4,X5} meets Y )
assume A7: Y in {X1,X2,X3,X4,X5} ; :: thesis: {X1,X2,X3,X4,X5} meets Y

now :: thesis: 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 ; :: thesis: ex y being set st
( y in {X1,X2,X3,X4,X5} & y in Y )

take y = X5; :: thesis: ( 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; :: thesis: verum

end;

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

take y = X1; :: thesis: ( 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; :: thesis: verum

end;

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

take y = X2; :: thesis: ( 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; :: thesis: verum

end;

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

take y = X3; :: thesis: ( 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; :: thesis: verum

end;

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

take y = X4; :: thesis: ( 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; :: thesis: verum

end;

end;

end;

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

end;

X1 in {X1,X2,X3,X4,X5} by ENUMSET1:def 3;
hence contradiction by A6, Th1; :: thesis: verum