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 A1: ( X1 in X2 & X2 in X3 & X3 in X4 & X4 in X5 & X5 in X1 ) ; :: thesis: contradiction
set Z = {X1,X2,X3,X4,X5};
A2: X1 in {X1,X2,X3,X4,X5} by ENUMSET1:def 3;
for Y being set st Y in {X1,X2,X3,X4,X5} holds
ex y being set st
( y in {X1,X2,X3,X4,X5} & y in Y )

proof

let Y be set ; :: thesis: ( Y in {X1,X2,X3,X4,X5} implies ex y being set st
( y in {X1,X2,X3,X4,X5} & y in Y ) )
assume A3: Y in {X1,X2,X3,X4,X5} ; :: thesis: ex y being set st
( y in {X1,X2,X3,X4,X5} & y in Y )

now

per cases ( Y = X1 or Y = X2 or Y = X3 or Y = X4 or Y = X5 ) by A3, ENUMSET1:def 3;

suppose A4: 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 A1, A4, ENUMSET1:def 3; :: thesis: verum

end;

suppose A5: 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, A5, ENUMSET1:def 3; :: thesis: verum

end;

suppose A6: 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 A1, A6, ENUMSET1:def 3; :: thesis: verum

end;

suppose A7: 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 A1, A7, ENUMSET1:def 3; :: thesis: verum

end;

suppose A8: 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 A1, A8, ENUMSET1:def 3; :: thesis: verum

end;

end;

end;

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

end;

hence contradiction by A2, TARSKI:7; :: thesis: verum