:: Consequences of Regularity Axiom
:: by Andrzej Trybulec
::
:: Received January 30, 2012
:: Copyright (c) 2012-2021 Association of Mizar Users

:: To jest po prostu "poprawne" sformulowanie aksjomatu regularnosci
:: W TARSKI 'misses' jest rozekspandowane, zeby uniknac definiowania 'misses'

theorem Th1: :: XREGULAR:1

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

proof end;

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

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

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

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

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

proof end;

:: Opuszczone dwa przypadki, ktore odpowiadaja irrefleksywnosci
:: i asymetri

theorem :: XREGULAR:7

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

proof end;

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 )

proof end;

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 )

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 )

proof end;