:: Consequences of Regularity Axiom
:: by Andrzej Trybulec
::
:: Received January 30, 2012
:: Copyright (c) 2012-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies TARSKI, XBOOLE_0;
notations TARSKI, XBOOLE_0, ENUMSET1;
constructors TARSKI, XBOOLE_0, ENUMSET1;
registrations XBOOLE_0;
requirements BOOLE;
begin
reserve x,y,X1,X2,X3,X4,X5,X6,Y,Y1,Y2,Y3,Y4,Y5,Z,Z1,Z2,Z3,Z4,Z5 for set;
reserve X for non empty set;
:: To jest po prostu "poprawne" sformulowanie aksjomatu regularnosci
:: W TARSKI 'misses' jest rozekspandowane, zeby uniknac definiowania 'misses'
theorem :: XREGULAR:1
ex Y st Y in X & Y misses X;
theorem :: XREGULAR:2
ex Y st Y in X & for Y1 st Y1 in Y holds Y1 misses X;
theorem :: XREGULAR:3
ex Y st Y in X & for Y1,Y2 st Y1 in Y2 & Y2 in Y holds Y1 misses X;
theorem :: XREGULAR:4
ex Y st Y in X &
for Y1,Y2,Y3 st Y1 in Y2 & Y2 in Y3 & Y3 in Y holds Y1 misses X;
theorem :: XREGULAR:5
ex Y st Y in X &
for Y1,Y2,Y3,Y4 st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y
holds Y1 misses X;
theorem :: XREGULAR:6
ex Y st Y in X &
for Y1,Y2,Y3,Y4,Y5 st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y
holds Y1 misses X;
:: Opuszczone dwa przypadki, ktore odpowiadaja irrefleksywnosci
:: i asymetri
theorem :: XREGULAR:7
not ( X1 in X2 & X2 in X3 & X3 in X1);
theorem :: XREGULAR:8
not ( X1 in X2 & X2 in X3 & X3 in X4 & X4 in X1);
theorem :: XREGULAR:9
not ( X1 in X2 & X2 in X3 & X3 in X4 & X4 in X5 & X5 in X1);
theorem :: XREGULAR:10
not ( X1 in X2 & X2 in X3 & X3 in X4 & X4 in X5 & X5 in X6 & X6 in X1);