:: XREGULAR semantic presentation

begin


theorem Th1: :: XREGULAR:1
for X being non empty set ex Y being set st
( Y in X & Y misses X )
proof
let X be non empty set ; ::_thesis: ex Y being set st
( Y in X & Y misses X )
consider x being set  such that
W: x in X by XBOOLE_0:def_1;
consider Y being set  such that
A1: ( Y in X & ( for x being set holds
( not x in X or not x in Y ) ) ) by TARSKI:2, W;
take  Y ; ::_thesis: ( Y in X & Y misses X )
thus  ( Y in X & Y misses X ) by A1, XBOOLE_0:3; ::_thesis: verum
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
let X be non empty set ; ::_thesis: ex Y being set st
( Y in X & ( for Y1 being set st Y1 in Y holds
Y1 misses X ) )
defpred S1[ set ] means $1 meets X;
consider Z being set  such that
A1: for Y being set holds
( Y in Z iff ( Y in union X & S1[Y] ) ) from XBOOLE_0:sch_1();
consider Y being set  such that
A2: Y in X \/ Z and
A3: Y misses X \/ Z by Th1;
assume A4: for Y being set holds
( not Y in X or ex Y1 being set st
( Y1 in Y & not Y1 misses X ) ) ; ::_thesis: contradiction
now__::_thesis:_not_Y_in_X
assume A5: Y in X ; ::_thesis: contradiction
then consider Y1 being set  such that
A6: Y1 in Y and
A7: not Y1 misses X by A4;
 Y1 in union X by A5, A6, TARSKI:def_4;
then  Y1 in Z by A1, A7;
then  Y1 in X \/ Z by XBOOLE_0:def_3;
hence  contradiction by A3, A6, XBOOLE_0:3; ::_thesis: verum
end;
then  Y in Z by A2, XBOOLE_0:def_3;
then  Y meets X by A1;
hence  contradiction by A3, XBOOLE_1:70; ::_thesis: verum
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
let X be non empty set ; ::_thesis: ex Y being set st
( Y in X & ( for Y1, Y2 being set st Y1 in Y2 & Y2 in Y holds
Y1 misses X ) )
defpred S1[ set ] means  ex Y1 being set st
( Y1 in $1 & Y1 meets X );
consider Z1 being set  such that
A1: for Y being set holds
( Y in Z1 iff ( Y in union X & S1[Y] ) ) from XBOOLE_0:sch_1();
defpred S2[ set ] means $1 meets X;
consider Z2 being set  such that
A2: for Y being set holds
( Y in Z2 iff ( Y in union (union X) & S2[Y] ) ) from XBOOLE_0:sch_1();
consider Y being set  such that
A3: Y in (X \/ Z1) \/ Z2 and
A4: Y misses (X \/ Z1) \/ Z2 by Th1;
A5: now__::_thesis:_not_Y_in_Z1
assume A6: Y in Z1 ; ::_thesis: contradiction
then consider Y1 being set  such that
A7: Y1 in Y and
A8: Y1 meets X by A1;
 Y in union X by A1, A6;
then  Y1 in union (union X) by A7, TARSKI:def_4;
then  Y1 in Z2 by A2, A8;
then  Y1 in (X \/ Z1) \/ Z2 by XBOOLE_0:def_3;
hence  contradiction by A4, A7, XBOOLE_0:3; ::_thesis: verum
end;
assume A9: for Y being set holds
( not Y in X or ex Y1, Y2 being set st
( Y1 in Y2 & Y2 in Y & not Y1 misses X ) ) ; ::_thesis: contradiction
A10: now__::_thesis:_not_Y_in_X
assume A11: Y in X ; ::_thesis: contradiction
then consider Y1, Y2 being set  such that
A12: Y1 in Y2 and
A13: Y2 in Y and
A14: not Y1 misses X by A9;
 Y2 in union X by A11, A13, TARSKI:def_4;
then  Y2 in Z1 by A1, A12, A14;
then  Y2 in X \/ Z1 by XBOOLE_0:def_3;
then  Y2 in (X \/ Z1) \/ Z2 by XBOOLE_0:def_3;
hence  contradiction by A4, A13, XBOOLE_0:3; ::_thesis: verum
end;
 Y in X \/ (Z1 \/ Z2) by A3, XBOOLE_1:4;
then  Y in Z1 \/ Z2 by A10, XBOOLE_0:def_3;
then  Y in Z2 by A5, XBOOLE_0:def_3;
then  Y meets X by A2;
then  Y meets X \/ Z1 by XBOOLE_1:70;
hence  contradiction by A4, XBOOLE_1:70; ::_thesis: verum
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
let X be non empty set ; ::_thesis: 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 ) )
defpred S1[ set ] means  ex Y1, Y2 being set st
( Y1 in Y2 & Y2 in $1 & Y1 meets X );
consider Z1 being set  such that
A1: for Y being set holds
( Y in Z1 iff ( Y in union X & S1[Y] ) ) from XBOOLE_0:sch_1();
defpred S2[ set ] means $1 meets X;
defpred S3[ set ] means  ex Y1 being set st
( Y1 in $1 & Y1 meets X );
consider Z2 being set  such that
A2: for Y being set holds
( Y in Z2 iff ( Y in union (union X) & S3[Y] ) ) from XBOOLE_0:sch_1();
consider Z3 being set  such that
A3: for Y being set holds
( Y in Z3 iff ( Y in union (union (union X)) & S2[Y] ) ) from XBOOLE_0:sch_1();
consider Y being set  such that
A4: Y in ((X \/ Z1) \/ Z2) \/ Z3 and
A5: Y misses ((X \/ Z1) \/ Z2) \/ Z3 by Th1;
A6: now__::_thesis:_not_Y_in_Z2
assume A7: Y in Z2 ; ::_thesis: contradiction
then consider Y1 being set  such that
A8: Y1 in Y and
A9: Y1 meets X by A2;
 Y in union (union X) by A2, A7;
then  Y1 in union (union (union X)) by A8, TARSKI:def_4;
then  Y1 in Z3 by A3, A9;
then  Y1 in ((X \/ Z1) \/ Z2) \/ Z3 by XBOOLE_0:def_3;
hence  contradiction by A5, A8, XBOOLE_0:3; ::_thesis: verum
end;
A10: now__::_thesis:_not_Y_in_Z1
assume A11: Y in Z1 ; ::_thesis: contradiction
then consider Y1, Y2 being set  such that
A12: Y1 in Y2 and
A13: Y2 in Y and
A14: Y1 meets X by A1;
 Y in union X by A1, A11;
then  Y2 in union (union X) by A13, TARSKI:def_4;
then  Y2 in Z2 by A2, A12, A14;
then  Y2 in (X \/ Z1) \/ Z2 by XBOOLE_0:def_3;
then  Y meets (X \/ Z1) \/ Z2 by A13, XBOOLE_0:3;
hence  contradiction by A5, XBOOLE_1:70; ::_thesis: verum
end;
set V = ((X \/ Z1) \/ Z2) \/ Z3;
A15: ((X \/ Z1) \/ Z2) \/ Z3 = (X \/ (Z1 \/ Z2)) \/ Z3 by XBOOLE_1:4
.= X \/ ((Z1 \/ Z2) \/ Z3) by XBOOLE_1:4 ;
assume A16: for Y being set holds
( not Y in X or ex Y1, Y2, Y3 being set st
( Y1 in Y2 & Y2 in Y3 & Y3 in Y & not Y1 misses X ) ) ; ::_thesis: contradiction
now__::_thesis:_not_Y_in_X
assume A17: Y in X ; ::_thesis: contradiction
then consider Y1, Y2, Y3 being set  such that
A18: ( Y1 in Y2 & Y2 in Y3 ) and
A19: Y3 in Y and
A20: not Y1 misses X by A16;
 Y3 in union X by A17, A19, TARSKI:def_4;
then  Y3 in Z1 by A1, A18, A20;
then  Y3 in X \/ Z1 by XBOOLE_0:def_3;
then  Y3 in (X \/ Z1) \/ Z2 by XBOOLE_0:def_3;
then  Y3 in ((X \/ Z1) \/ Z2) \/ Z3 by XBOOLE_0:def_3;
hence  contradiction by A5, A19, XBOOLE_0:3; ::_thesis: verum
end;
then  Y in (Z1 \/ Z2) \/ Z3 by A15, A4, XBOOLE_0:def_3;
then  Y in Z1 \/ (Z2 \/ Z3) by XBOOLE_1:4;
then  Y in Z2 \/ Z3 by A10, XBOOLE_0:def_3;
then  Y in Z3 by A6, XBOOLE_0:def_3;
then  Y meets X by A3;
hence  contradiction by A15, A5, XBOOLE_1:70; ::_thesis: verum
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
let X be non empty set ; ::_thesis: 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 ) )
defpred S1[ set ] means  ex Y1, Y2, Y3 being set st
( Y1 in Y2 & Y2 in Y3 & Y3 in $1 & Y1 meets X );
consider Z1 being set  such that
A1: for Y being set holds
( Y in Z1 iff ( Y in union X & S1[Y] ) ) from XBOOLE_0:sch_1();
defpred S2[ set ] means $1 meets X;
defpred S3[ set ] means  ex Y1 being set st
( Y1 in $1 & Y1 meets X );
defpred S4[ set ] means  ex Y1, Y2 being set st
( Y1 in Y2 & Y2 in $1 & Y1 meets X );
consider Z2 being set  such that
A2: for Y being set holds
( Y in Z2 iff ( Y in union (union X) & S4[Y] ) ) from XBOOLE_0:sch_1();
consider Z4 being set  such that
A3: for Y being set holds
( Y in Z4 iff ( Y in union (union (union (union X))) & S2[Y] ) ) from XBOOLE_0:sch_1();
consider Z3 being set  such that
A4: for Y being set holds
( Y in Z3 iff ( Y in union (union (union X)) & S3[Y] ) ) from XBOOLE_0:sch_1();
consider Y being set  such that
A5: Y in (((X \/ Z1) \/ Z2) \/ Z3) \/ Z4 and
A6: Y misses (((X \/ Z1) \/ Z2) \/ Z3) \/ Z4 by Th1;
A7: now__::_thesis:_not_Y_in_Z3
assume A8: Y in Z3 ; ::_thesis: contradiction
then consider Y1 being set  such that
A9: Y1 in Y and
A10: Y1 meets X by A4;
 Y in union (union (union X)) by A4, A8;
then  Y1 in union (union (union (union X))) by A9, TARSKI:def_4;
then  Y1 in Z4 by A3, A10;
then  Y1 in (((X \/ Z1) \/ Z2) \/ Z3) \/ Z4 by XBOOLE_0:def_3;
hence  contradiction by A6, A9, XBOOLE_0:3; ::_thesis: verum
end;
A11: now__::_thesis:_not_Y_in_Z1
assume A12: Y in Z1 ; ::_thesis: contradiction
then consider Y1, Y2, Y3 being set  such that
A13: ( Y1 in Y2 & Y2 in Y3 ) and
A14: Y3 in Y and
A15: Y1 meets X by A1;
 Y in union X by A1, A12;
then  Y3 in union (union X) by A14, TARSKI:def_4;
then  Y3 in Z2 by A2, A13, A15;
then  Y3 in (X \/ Z1) \/ Z2 by XBOOLE_0:def_3;
then  Y meets (X \/ Z1) \/ Z2 by A14, XBOOLE_0:3;
then  Y meets ((X \/ Z1) \/ Z2) \/ Z3 by XBOOLE_1:70;
hence  contradiction by A6, XBOOLE_1:70; ::_thesis: verum
end;
A16: (((X \/ Z1) \/ Z2) \/ Z3) \/ Z4 = ((X \/ (Z1 \/ Z2)) \/ Z3) \/ Z4 by XBOOLE_1:4
.= (X \/ ((Z1 \/ Z2) \/ Z3)) \/ Z4 by XBOOLE_1:4
.= X \/ (((Z1 \/ Z2) \/ Z3) \/ Z4) by XBOOLE_1:4 ;
A17: now__::_thesis:_not_Y_in_Z2
assume A18: Y in Z2 ; ::_thesis: contradiction
then consider Y1, Y2 being set  such that
A19: Y1 in Y2 and
A20: Y2 in Y and
A21: Y1 meets X by A2;
 Y in union (union X) by A2, A18;
then  Y2 in union (union (union X)) by A20, TARSKI:def_4;
then  Y2 in Z3 by A4, A19, A21;
then  Y2 in ((X \/ Z1) \/ Z2) \/ Z3 by XBOOLE_0:def_3;
then  Y meets ((X \/ Z1) \/ Z2) \/ Z3 by A20, XBOOLE_0:3;
hence  contradiction by A6, XBOOLE_1:70; ::_thesis: verum
end;
assume A22: for Y being set holds
( not Y in X or ex Y1, Y2, Y3, Y4 being set st
( Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y & not Y1 misses X ) ) ; ::_thesis: contradiction
now__::_thesis:_not_Y_in_X
assume A23: Y in X ; ::_thesis: contradiction
then consider Y1, Y2, Y3, Y4 being set  such that
A24: ( Y1 in Y2 & Y2 in Y3 & Y3 in Y4 ) and
A25: Y4 in Y and
A26: not Y1 misses X by A22;
 Y4 in union X by A23, A25, TARSKI:def_4;
then  Y4 in Z1 by A1, A24, A26;
then  Y4 in X \/ Z1 by XBOOLE_0:def_3;
then  Y4 in (X \/ Z1) \/ Z2 by XBOOLE_0:def_3;
then  Y4 in ((X \/ Z1) \/ Z2) \/ Z3 by XBOOLE_0:def_3;
then  Y4 in (((X \/ Z1) \/ Z2) \/ Z3) \/ Z4 by XBOOLE_0:def_3;
hence  contradiction by A6, A25, XBOOLE_0:3; ::_thesis: verum
end;
then  Y in ((Z1 \/ Z2) \/ Z3) \/ Z4 by A16, A5, XBOOLE_0:def_3;
then  Y in (Z1 \/ (Z2 \/ Z3)) \/ Z4 by XBOOLE_1:4;
then  Y in Z1 \/ ((Z2 \/ Z3) \/ Z4) by XBOOLE_1:4;
then  Y in (Z2 \/ Z3) \/ Z4 by A11, XBOOLE_0:def_3;
then  Y in Z2 \/ (Z3 \/ Z4) by XBOOLE_1:4;
then  Y in Z3 \/ Z4 by A17, XBOOLE_0:def_3;
then  Y in Z4 by A7, XBOOLE_0:def_3;
then  Y meets X by A3;
hence  contradiction by A16, A6, XBOOLE_1:70; ::_thesis: verum
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
let X be non empty set ; ::_thesis: 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 ) )
defpred S1[ set ] means  ex Y1, Y2, Y3, Y4 being set st
( Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in $1 & Y1 meets X );
consider Z1 being set  such that
A1: for Y being set holds
( Y in Z1 iff ( Y in union X & S1[Y] ) ) from XBOOLE_0:sch_1();
defpred S2[ set ] means $1 meets X;
defpred S3[ set ] means  ex Y1 being set st
( Y1 in $1 & Y1 meets X );
defpred S4[ set ] means  ex Y1, Y2 being set st
( Y1 in Y2 & Y2 in $1 & Y1 meets X );
defpred S5[ set ] means  ex Y1, Y2, Y3 being set st
( Y1 in Y2 & Y2 in Y3 & Y3 in $1 & Y1 meets X );
consider Z2 being set  such that
A2: for Y being set holds
( Y in Z2 iff ( Y in union (union X) & S5[Y] ) ) from XBOOLE_0:sch_1();
consider Z5 being set  such that
A3: for Y being set holds
( Y in Z5 iff ( Y in union (union (union (union (union X)))) & S2[Y] ) ) from XBOOLE_0:sch_1();
consider Z3 being set  such that
A4: for Y being set holds
( Y in Z3 iff ( Y in union (union (union X)) & S4[Y] ) ) from XBOOLE_0:sch_1();
consider Z4 being set  such that
A5: for Y being set holds
( Y in Z4 iff ( Y in union (union (union (union X))) & S3[Y] ) ) from XBOOLE_0:sch_1();
set V = ((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5;
consider Y being set  such that
A6: Y in ((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5 and
A7: Y misses ((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5 by Th1;
A8: ((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5 = (((X \/ (Z1 \/ Z2)) \/ Z3) \/ Z4) \/ Z5 by XBOOLE_1:4
.= ((X \/ ((Z1 \/ Z2) \/ Z3)) \/ Z4) \/ Z5 by XBOOLE_1:4
.= (X \/ (((Z1 \/ Z2) \/ Z3) \/ Z4)) \/ Z5 by XBOOLE_1:4
.= X \/ ((((Z1 \/ Z2) \/ Z3) \/ Z4) \/ Z5) by XBOOLE_1:4 ;
A9: now__::_thesis:_not_Y_in_Z1
assume A10: Y in Z1 ; ::_thesis: contradiction
then consider Y1, Y2, Y3, Y4 being set  such that
A11: ( Y1 in Y2 & Y2 in Y3 & Y3 in Y4 ) and
A12: Y4 in Y and
A13: Y1 meets X by A1;
 Y in union X by A1, A10;
then  Y4 in union (union X) by A12, TARSKI:def_4;
then  Y4 in Z2 by A2, A11, A13;
then  Y4 in (X \/ Z1) \/ Z2 by XBOOLE_0:def_3;
then  Y meets (X \/ Z1) \/ Z2 by A12, XBOOLE_0:3;
then  Y meets ((X \/ Z1) \/ Z2) \/ Z3 by XBOOLE_1:70;
then  Y meets (((X \/ Z1) \/ Z2) \/ Z3) \/ Z4 by XBOOLE_1:70;
hence  contradiction by A7, XBOOLE_1:70; ::_thesis: verum
end;
A14: now__::_thesis:_not_Y_in_Z2
assume A15: Y in Z2 ; ::_thesis: contradiction
then consider Y1, Y2, Y3 being set  such that
A16: ( Y1 in Y2 & Y2 in Y3 ) and
A17: Y3 in Y and
A18: Y1 meets X by A2;
 Y in union (union X) by A2, A15;
then  Y3 in union (union (union X)) by A17, TARSKI:def_4;
then  Y3 in Z3 by A4, A16, A18;
then  Y3 in ((X \/ Z1) \/ Z2) \/ Z3 by XBOOLE_0:def_3;
then  Y3 in (((X \/ Z1) \/ Z2) \/ Z3) \/ Z4 by XBOOLE_0:def_3;
then  Y3 in ((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5 by XBOOLE_0:def_3;
hence  contradiction by A7, A17, XBOOLE_0:3; ::_thesis: verum
end;
A19: now__::_thesis:_not_Y_in_Z3
assume A20: Y in Z3 ; ::_thesis: contradiction
then consider Y1, Y2 being set  such that
A21: Y1 in Y2 and
A22: Y2 in Y and
A23: Y1 meets X by A4;
 Y in union (union (union X)) by A4, A20;
then  Y2 in union (union (union (union X))) by A22, TARSKI:def_4;
then  Y2 in Z4 by A5, A21, A23;
then  Y2 in (((X \/ Z1) \/ Z2) \/ Z3) \/ Z4 by XBOOLE_0:def_3;
then  Y2 in ((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5 by XBOOLE_0:def_3;
hence  contradiction by A7, A22, XBOOLE_0:3; ::_thesis: verum
end;
A24: now__::_thesis:_not_Y_in_Z4
assume A25: Y in Z4 ; ::_thesis: contradiction
then consider Y1 being set  such that
A26: Y1 in Y and
A27: Y1 meets X by A5;
 Y in union (union (union (union X))) by A5, A25;
then  Y1 in union (union (union (union (union X)))) by A26, TARSKI:def_4;
then  Y1 in Z5 by A3, A27;
then  Y1 in ((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5 by XBOOLE_0:def_3;
hence  contradiction by A7, A26, XBOOLE_0:3; ::_thesis: verum
end;
assume A28: for Y being set holds
( not Y in X or ex Y1, Y2, Y3, Y4, Y5 being set st
( Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y & not Y1 misses X ) ) ; ::_thesis: contradiction
now__::_thesis:_not_Y_in_X
assume A29: Y in X ; ::_thesis: contradiction
then consider Y1, Y2, Y3, Y4, Y5 being set  such that
A30: ( Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 ) and
A31: Y5 in Y and
A32: not Y1 misses X by A28;
 Y5 in union X by A29, A31, TARSKI:def_4;
then  Y5 in Z1 by A1, A30, A32;
then  Y5 in X \/ Z1 by XBOOLE_0:def_3;
then  Y5 in (X \/ Z1) \/ Z2 by XBOOLE_0:def_3;
then  Y5 in ((X \/ Z1) \/ Z2) \/ Z3 by XBOOLE_0:def_3;
then  Y meets ((X \/ Z1) \/ Z2) \/ Z3 by A31, XBOOLE_0:3;
then  Y meets (((X \/ Z1) \/ Z2) \/ Z3) \/ Z4 by XBOOLE_1:70;
hence  contradiction by A7, XBOOLE_1:70; ::_thesis: verum
end;
then  Y in (((Z1 \/ Z2) \/ Z3) \/ Z4) \/ Z5 by A8, A6, XBOOLE_0:def_3;
then  Y in ((Z1 \/ (Z2 \/ Z3)) \/ Z4) \/ Z5 by XBOOLE_1:4;
then  Y in (Z1 \/ ((Z2 \/ Z3) \/ Z4)) \/ Z5 by XBOOLE_1:4;
then  Y in Z1 \/ (((Z2 \/ Z3) \/ Z4) \/ Z5) by XBOOLE_1:4;
then  Y in ((Z2 \/ Z3) \/ Z4) \/ Z5 by A9, XBOOLE_0:def_3;
then  Y in (Z2 \/ (Z3 \/ Z4)) \/ Z5 by XBOOLE_1:4;
then  Y in Z2 \/ ((Z3 \/ Z4) \/ Z5) by XBOOLE_1:4;
then  Y in (Z3 \/ Z4) \/ Z5 by A14, XBOOLE_0:def_3;
then  Y in Z3 \/ (Z4 \/ Z5) by XBOOLE_1:4;
then  Y in Z4 \/ Z5 by A19, XBOOLE_0:def_3;
then  Y in Z5 by A24, XBOOLE_0:def_3;
then  Y meets X by A3;
hence  contradiction by A8, A7, XBOOLE_1:70; ::_thesis: verum
end;

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
let X1, X2, X3 be set ; ::_thesis: ( not X1 in X2 or not X2 in X3 or not X3 in X1 )
A1: ( X2 in {X1,X2,X3} & X3 in {X1,X2,X3} ) by ENUMSET1:def_1;
A2: X1 in {X1,X2,X3} by ENUMSET1:def_1;
then consider T being set  such that
A3: T in {X1,X2,X3} and
A4: {X1,X2,X3} misses T by Th1;
 ( T = X1 or T = X2 or T = X3 ) by A3, ENUMSET1:def_1;
hence  ( not X1 in X2 or not X2 in X3 or not X3 in X1 ) by A2, A1, A4, XBOOLE_0:3; ::_thesis: verum
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
let X1, X2, X3, X4 be set ; ::_thesis: ( not X1 in X2 or not X2 in X3 or not X3 in X4 or not X4 in X1 )
A1: ( X2 in {X1,X2,X3,X4} & X3 in {X1,X2,X3,X4} ) by ENUMSET1:def_2;
A2: X4 in {X1,X2,X3,X4} by ENUMSET1:def_2;
A3: X1 in {X1,X2,X3,X4} by ENUMSET1:def_2;
then consider T being set  such that
A4: T in {X1,X2,X3,X4} and
A5: {X1,X2,X3,X4} misses T by Th1;
 ( T = X1 or T = X2 or T = X3 or T = X4 ) by A4, ENUMSET1:def_2;
hence  ( not X1 in X2 or not X2 in X3 or not X3 in X4 or not X4 in X1 ) by A3, A1, A2, A5, XBOOLE_0:3; ::_thesis: verum
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
let X1, X2, X3, X4, X5 be set ; ::_thesis: ( not X1 in X2 or not X2 in X3 or not X3 in X4 or not X4 in X5 or not X5 in X1 )
assume that
A1: X1 in X2 and
A2: X2 in X3 and
A3: X3 in X4 and
A4: X4 in X5 and
A5: X5 in X1 ; ::_thesis: contradiction
set Z = {X1,X2,X3,X4,X5};
A6: for Y being set st Y in {X1,X2,X3,X4,X5} holds
{X1,X2,X3,X4,X5} meets Y
proof
let Y be set ; ::_thesis: ( Y in {X1,X2,X3,X4,X5} implies {X1,X2,X3,X4,X5} meets Y )
assume A7: Y in {X1,X2,X3,X4,X5} ; ::_thesis: {X1,X2,X3,X4,X5} meets Y
now__::_thesis:_ex_y_being_set_st_
(_y_in_{X1,X2,X3,X4,X5}_&_y_in_Y_)
percases ( Y = X1 or Y = X2 or Y = X3 or Y = X4 or Y = X5 ) by A7, ENUMSET1:def_3;
supposeA8: Y = X1 ; ::_thesis: ex y being set st
( y in {X1,X2,X3,X4,X5} & y in Y )
take y = X5; ::_thesis: ( y in {X1,X2,X3,X4,X5} & y in Y )
thus  ( y in {X1,X2,X3,X4,X5} & y in Y ) by A5, A8, ENUMSET1:def_3; ::_thesis: verum
end;
supposeA9: Y = X2 ; ::_thesis: ex y being set st
( y in {X1,X2,X3,X4,X5} & y in Y )
take y = X1; ::_thesis: ( y in {X1,X2,X3,X4,X5} & y in Y )
thus  ( y in {X1,X2,X3,X4,X5} & y in Y ) by A1, A9, ENUMSET1:def_3; ::_thesis: verum
end;
supposeA10: Y = X3 ; ::_thesis: ex y being set st
( y in {X1,X2,X3,X4,X5} & y in Y )
take y = X2; ::_thesis: ( y in {X1,X2,X3,X4,X5} & y in Y )
thus  ( y in {X1,X2,X3,X4,X5} & y in Y ) by A2, A10, ENUMSET1:def_3; ::_thesis: verum
end;
supposeA11: Y = X4 ; ::_thesis: ex y being set st
( y in {X1,X2,X3,X4,X5} & y in Y )
take y = X3; ::_thesis: ( y in {X1,X2,X3,X4,X5} & y in Y )
thus  ( y in {X1,X2,X3,X4,X5} & y in Y ) by A3, A11, ENUMSET1:def_3; ::_thesis: verum
end;
supposeA12: Y = X5 ; ::_thesis: ex y being set st
( y in {X1,X2,X3,X4,X5} & y in Y )
take y = X4; ::_thesis: ( y in {X1,X2,X3,X4,X5} & y in Y )
thus  ( y in {X1,X2,X3,X4,X5} & y in Y ) by A4, A12, ENUMSET1:def_3; ::_thesis: verum
end;
end;
end;
hence  {X1,X2,X3,X4,X5} meets Y by XBOOLE_0:3; ::_thesis: verum
end;
 X1 in {X1,X2,X3,X4,X5} by ENUMSET1:def_3;
hence  contradiction by A6, Th1; ::_thesis: verum
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
let X1, X2, X3, X4, X5, X6 be set ; ::_thesis: ( 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 )
assume that
A1: X1 in X2 and
A2: X2 in X3 and
A3: X3 in X4 and
A4: X4 in X5 and
A5: X5 in X6 and
A6: X6 in X1 ; ::_thesis: contradiction
set Z = {X1,X2,X3,X4,X5,X6};
A7: for Y being set st Y in {X1,X2,X3,X4,X5,X6} holds
{X1,X2,X3,X4,X5,X6} meets Y
proof
let Y be set ; ::_thesis: ( Y in {X1,X2,X3,X4,X5,X6} implies {X1,X2,X3,X4,X5,X6} meets Y )
assume A8: Y in {X1,X2,X3,X4,X5,X6} ; ::_thesis: {X1,X2,X3,X4,X5,X6} meets Y
now__::_thesis:_ex_y_being_set_st_
(_y_in_{X1,X2,X3,X4,X5,X6}_&_y_in_Y_)
percases ( Y = X1 or Y = X2 or Y = X3 or Y = X4 or Y = X5 or Y = X6 ) by A8, ENUMSET1:def_4;
supposeA9: Y = X1 ; ::_thesis: ex y being set st
( y in {X1,X2,X3,X4,X5,X6} & y in Y )
take y = X6; ::_thesis: ( y in {X1,X2,X3,X4,X5,X6} & y in Y )
thus  ( y in {X1,X2,X3,X4,X5,X6} & y in Y ) by A6, A9, ENUMSET1:def_4; ::_thesis: verum
end;
supposeA10: Y = X2 ; ::_thesis: ex y being set st
( y in {X1,X2,X3,X4,X5,X6} & y in Y )
take y = X1; ::_thesis: ( y in {X1,X2,X3,X4,X5,X6} & y in Y )
thus  ( y in {X1,X2,X3,X4,X5,X6} & y in Y ) by A1, A10, ENUMSET1:def_4; ::_thesis: verum
end;
supposeA11: Y = X3 ; ::_thesis: ex y being set st
( y in {X1,X2,X3,X4,X5,X6} & y in Y )
take y = X2; ::_thesis: ( y in {X1,X2,X3,X4,X5,X6} & y in Y )
thus  ( y in {X1,X2,X3,X4,X5,X6} & y in Y ) by A2, A11, ENUMSET1:def_4; ::_thesis: verum
end;
supposeA12: Y = X4 ; ::_thesis: ex y being set st
( y in {X1,X2,X3,X4,X5,X6} & y in Y )
take y = X3; ::_thesis: ( y in {X1,X2,X3,X4,X5,X6} & y in Y )
thus  ( y in {X1,X2,X3,X4,X5,X6} & y in Y ) by A3, A12, ENUMSET1:def_4; ::_thesis: verum
end;
supposeA13: Y = X5 ; ::_thesis: ex y being set st
( y in {X1,X2,X3,X4,X5,X6} & y in Y )
take y = X4; ::_thesis: ( y in {X1,X2,X3,X4,X5,X6} & y in Y )
thus  ( y in {X1,X2,X3,X4,X5,X6} & y in Y ) by A4, A13, ENUMSET1:def_4; ::_thesis: verum
end;
supposeA14: Y = X6 ; ::_thesis: ex y being set st
( y in {X1,X2,X3,X4,X5,X6} & y in Y )
take y = X5; ::_thesis: ( y in {X1,X2,X3,X4,X5,X6} & y in Y )
thus  ( y in {X1,X2,X3,X4,X5,X6} & y in Y ) by A5, A14, ENUMSET1:def_4; ::_thesis: verum
end;
end;
end;
hence  {X1,X2,X3,X4,X5,X6} meets Y by XBOOLE_0:3; ::_thesis: verum
end;
 X1 in {X1,X2,X3,X4,X5,X6} by ENUMSET1:def_4;
hence  contradiction by A7, Th1; ::_thesis: verum
end;