XREGULAR

theorem :: XREGULAR:1

for X being ( ( non empty ) ( non empty ) set ) ex Y being ( ( ) ( ) set ) st
( Y : ( ( ) ( ) set ) in X : ( ( non empty ) ( non empty ) set ) & Y : ( ( ) ( ) set ) misses X : ( ( non empty ) ( non empty ) set ) ) ;

theorem :: XREGULAR:2

for X being ( ( non empty ) ( non empty ) set ) ex Y being ( ( ) ( ) set ) st
( Y : ( ( ) ( ) set ) in X : ( ( non empty ) ( non empty ) set ) & ( for Y1 being ( ( ) ( ) set ) st Y1 : ( ( ) ( ) set ) in Y : ( ( ) ( ) set ) holds
Y1 : ( ( ) ( ) set ) misses X : ( ( non empty ) ( non empty ) set ) ) ) ;

theorem :: XREGULAR:3

for X being ( ( non empty ) ( non empty ) set ) ex Y being ( ( ) ( ) set ) st
( Y : ( ( ) ( ) set ) in X : ( ( non empty ) ( non empty ) set ) & ( for Y1, Y2 being ( ( ) ( ) set ) st Y1 : ( ( ) ( ) set ) in Y2 : ( ( ) ( ) set ) & Y2 : ( ( ) ( ) set ) in Y : ( ( ) ( ) set ) holds
Y1 : ( ( ) ( ) set ) misses X : ( ( non empty ) ( non empty ) set ) ) ) ;

theorem :: XREGULAR:4

for X being ( ( non empty ) ( non empty ) set ) ex Y being ( ( ) ( ) set ) st
( Y : ( ( ) ( ) set ) in X : ( ( non empty ) ( non empty ) set ) & ( for Y1, Y2, Y3 being ( ( ) ( ) set ) st Y1 : ( ( ) ( ) set ) in Y2 : ( ( ) ( ) set ) & Y2 : ( ( ) ( ) set ) in Y3 : ( ( ) ( ) set ) & Y3 : ( ( ) ( ) set ) in Y : ( ( ) ( ) set ) holds
Y1 : ( ( ) ( ) set ) misses X : ( ( non empty ) ( non empty ) set ) ) ) ;

theorem :: XREGULAR:5

for X being ( ( non empty ) ( non empty ) set ) ex Y being ( ( ) ( ) set ) st
( Y : ( ( ) ( ) set ) in X : ( ( non empty ) ( non empty ) set ) & ( for Y1, Y2, Y3, Y4 being ( ( ) ( ) set ) st Y1 : ( ( ) ( ) set ) in Y2 : ( ( ) ( ) set ) & Y2 : ( ( ) ( ) set ) in Y3 : ( ( ) ( ) set ) & Y3 : ( ( ) ( ) set ) in Y4 : ( ( ) ( ) set ) & Y4 : ( ( ) ( ) set ) in Y : ( ( ) ( ) set ) holds
Y1 : ( ( ) ( ) set ) misses X : ( ( non empty ) ( non empty ) set ) ) ) ;

theorem :: XREGULAR:6

for X being ( ( non empty ) ( non empty ) set ) ex Y being ( ( ) ( ) set ) st
( Y : ( ( ) ( ) set ) in X : ( ( non empty ) ( non empty ) set ) & ( for Y1, Y2, Y3, Y4, Y5 being ( ( ) ( ) set ) st Y1 : ( ( ) ( ) set ) in Y2 : ( ( ) ( ) set ) & Y2 : ( ( ) ( ) set ) in Y3 : ( ( ) ( ) set ) & Y3 : ( ( ) ( ) set ) in Y4 : ( ( ) ( ) set ) & Y4 : ( ( ) ( ) set ) in Y5 : ( ( ) ( ) set ) & Y5 : ( ( ) ( ) set ) in Y : ( ( ) ( ) set ) holds
Y1 : ( ( ) ( ) set ) misses X : ( ( non empty ) ( non empty ) set ) ) ) ;

theorem :: XREGULAR:7

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

theorem :: XREGULAR:8

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

theorem :: XREGULAR:9

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

theorem :: XREGULAR:10

for X1, X2, X3, X4, X5, X6 being ( ( ) ( ) set ) holds
( not X1 : ( ( ) ( ) set ) in X2 : ( ( ) ( ) set ) or not X2 : ( ( ) ( ) set ) in X3 : ( ( ) ( ) set ) or not X3 : ( ( ) ( ) set ) in X4 : ( ( ) ( ) set ) or not X4 : ( ( ) ( ) set ) in X5 : ( ( ) ( ) set ) or not X5 : ( ( ) ( ) set ) in X6 : ( ( ) ( ) set ) or not X6 : ( ( ) ( ) set ) in X1 : ( ( ) ( ) set ) ) ;