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