:: by Andrzej Trybulec

::

:: Received January 30, 2012

:: Copyright (c) 2012-2021 Association of Mizar Users

theorem :: XREGULAR:2

for X being non empty set ex Y being set st

( Y in X & ( for Y1 being set st Y1 in Y holds

Y1 misses X ) )

( Y in X & ( for Y1 being set st Y1 in Y holds

Y1 misses X ) )

proof end;

theorem :: XREGULAR:3

for X being non empty set ex Y being set st

( Y in X & ( for Y1, Y2 being set st Y1 in Y2 & Y2 in Y holds

Y1 misses X ) )

( Y in X & ( for Y1, Y2 being set st Y1 in Y2 & Y2 in Y holds

Y1 misses X ) )

proof end;

theorem :: XREGULAR:4

for X being non empty set ex Y being set st

( Y in X & ( for Y1, Y2, Y3 being set st Y1 in Y2 & Y2 in Y3 & Y3 in Y holds

Y1 misses X ) )

( Y in X & ( for Y1, Y2, Y3 being set st Y1 in Y2 & Y2 in Y3 & Y3 in Y holds

Y1 misses X ) )

proof end;

theorem :: XREGULAR:5

for X being non empty set ex Y being set st

( Y in X & ( for Y1, Y2, Y3, Y4 being set st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y holds

Y1 misses X ) )

( Y in X & ( for Y1, Y2, Y3, Y4 being set st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y holds

Y1 misses X ) )

proof end;

theorem :: XREGULAR:6

for X being non empty set ex Y being set st

( Y in X & ( for Y1, Y2, Y3, Y4, Y5 being set st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y holds

Y1 misses X ) )

( Y in X & ( for Y1, Y2, Y3, Y4, Y5 being set st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y holds

Y1 misses X ) )

proof end;

:: Opuszczone dwa przypadki, ktore odpowiadaja irrefleksywnosci

:: i asymetri

:: i asymetri

theorem :: XREGULAR:9

for X1, X2, X3, X4, X5 being set holds

( not X1 in X2 or not X2 in X3 or not X3 in X4 or not X4 in X5 or not X5 in X1 )

( not X1 in X2 or not X2 in X3 or not X3 in X4 or not X4 in X5 or not X5 in X1 )

proof end;

theorem :: XREGULAR:10

for X1, X2, X3, X4, X5, X6 being set holds

( 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 )

( 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 )

proof end;

:: W TARSKI 'misses' jest rozekspandowane, zeby uniknac definiowania 'misses'