theorem :: XREGULAR:8

for X1, X2, X3, X4 being set holds
( not X1 in X2 or not X2 in X3 or not X3 in X4 or not X4 in X1 )