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


begin

:: 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 )
proofend;

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

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

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

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

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

:: 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 )
proofend;

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

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

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