:: PARTIT1 semantic presentation

begin


theorem Th1: :: PARTIT1:1
for Y being non empty set
for PA being a_partition of Y
for X, V being set st X in PA & V in PA & X c= V holds
X = V
proof
let Y be non empty set ; ::_thesis: for PA being a_partition of Y
for X, V being set st X in PA & V in PA & X c= V holds
X = V
let PA be a_partition of Y; ::_thesis: for X, V being set st X in PA & V in PA & X c= V holds
X = V
let X, V be set ; ::_thesis: ( X in PA & V in PA & X c= V implies X = V )
assume that
A1: X in PA and
A2: V in PA and
A3: X c= V ; ::_thesis: X = V
A4: ( X = V or X misses V ) by A1, A2, EQREL_1:def_4;
set x = the Element of X;
 X <> {} by A1, EQREL_1:def_4;
then  the Element of X in X ;
hence  X = V by A3, A4, XBOOLE_0:3; ::_thesis: verum
end;

notation
let SFX, SFY be set ;
synonym SFX '<' SFY for SFX is_finer_than SFY;
synonym SFY '>' SFX for SFX is_finer_than SFY;
end;

theorem Th2: :: PARTIT1:2
for SFX being set holds union (SFX \ {{}}) = union SFX
proof
let SFX be set ; ::_thesis: union (SFX \ {{}}) = union SFX
A1: union (SFX \ {{}}) c= union SFX
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in union (SFX \ {{}}) or y in union SFX )
assume  y in union (SFX \ {{}}) ; ::_thesis: y in union SFX
then  ex z being set st
( y in z & z in SFX \ {{}} ) by TARSKI:def_4;
hence  y in union SFX by TARSKI:def_4; ::_thesis: verum
end;
 union SFX c= union (SFX \ {{}})
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in union SFX or y in union (SFX \ {{}}) )
assume  y in union SFX ; ::_thesis: y in union (SFX \ {{}})
then consider X being set  such that
A2: y in X and
A3: X in SFX by TARSKI:def_4;
 not X in {{}} by A2, TARSKI:def_1;
then  X in SFX \ {{}} by A3, XBOOLE_0:def_5;
hence  y in union (SFX \ {{}}) by A2, TARSKI:def_4; ::_thesis: verum
end;
hence  union (SFX \ {{}}) = union SFX by A1, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th3: :: PARTIT1:3
for Y being non empty set
for PA, PB being a_partition of Y st PA '>' PB & PB '>' PA holds
PB c= PA
proof
let Y be non empty set ; ::_thesis: for PA, PB being a_partition of Y st PA '>' PB & PB '>' PA holds
PB c= PA
let PA, PB be a_partition of Y; ::_thesis: ( PA '>' PB & PB '>' PA implies PB c= PA )
assume that
A1: PA '>' PB and
A2: PB '>' PA ; ::_thesis: PB c= PA
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in PB or x in PA )
assume A3: x in PB ; ::_thesis: x in PA
then consider V being set  such that
A4: V in PA and
A5: x c= V by A1, SETFAM_1:def_2;
consider W being set  such that
A6: W in PB and
A7: V c= W by A2, A4, SETFAM_1:def_2;
 x = W by A3, A5, A6, A7, Th1, XBOOLE_1:1;
hence  x in PA by A4, A5, A7, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th4: :: PARTIT1:4
for Y being non empty set
for PA, PB being a_partition of Y st PA '>' PB & PB '>' PA holds
PA = PB
proof
let Y be non empty set ; ::_thesis: for PA, PB being a_partition of Y st PA '>' PB & PB '>' PA holds
PA = PB
let PA, PB be a_partition of Y; ::_thesis: ( PA '>' PB & PB '>' PA implies PA = PB )
assume  ( PA '>' PB & PB '>' PA ) ; ::_thesis: PA = PB
then  ( PB c= PA & PA c= PB ) by Th3;
hence  PA = PB by XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th5: :: PARTIT1:5
for Y being non empty set
for PA, PB being a_partition of Y st PA '>' PB holds
PA is_coarser_than PB
proof
let Y be non empty set ; ::_thesis: for PA, PB being a_partition of Y st PA '>' PB holds
PA is_coarser_than PB
let PA, PB be a_partition of Y; ::_thesis: ( PA '>' PB implies PA is_coarser_than PB )
assume A1: PA '>' PB ; ::_thesis: PA is_coarser_than PB
 for x being set st x in PA holds
ex y being set st
( y in PB & y c= x )
proof
let x be set ; ::_thesis: ( x in PA implies ex y being set st
( y in PB & y c= x ) )
assume A2: x in PA ; ::_thesis: ex y being set st
( y in PB & y c= x )
then A3: x <> {} by EQREL_1:def_4;
set u = the Element of x;
A4: the Element of x in x by A3;
 union PB = Y by EQREL_1:def_4;
then consider y being set  such that
A5: the Element of x in y and
A6: y in PB by A2, A4, TARSKI:def_4;
consider z being set  such that
A7: z in PA and
A8: y c= z by A1, A6, SETFAM_1:def_2;
 ( x = z or x misses z ) by A2, A7, EQREL_1:def_4;
hence  ex y being set st
( y in PB & y c= x ) by A3, A5, A6, A8, XBOOLE_0:3; ::_thesis: verum
end;
hence  PA is_coarser_than PB by SETFAM_1:def_3; ::_thesis: verum
end;

definition
let Y be non empty set ;
let PA be a_partition of Y;
let b be set ;
predb is_a_dependent_set_of PA means :Def1: :: PARTIT1:def 1
 ex B being set st
( B c= PA & B <> {} & b = union B );
end;

:: deftheorem Def1 defines is_a_dependent_set_of PARTIT1:def_1_:_
 for Y being non empty set
for PA being a_partition of Y
for b being set holds
( b is_a_dependent_set_of PA iff ex B being set st
( B c= PA & B <> {} & b = union B ) );

definition
let Y be non empty set ;
let PA, PB be a_partition of Y;
let b be set ;
predb is_min_depend PA,PB means :Def2: :: PARTIT1:def 2
( b is_a_dependent_set_of PA & b is_a_dependent_set_of PB & ( for d being set st d c= b & d is_a_dependent_set_of PA & d is_a_dependent_set_of PB holds
d = b ) );
end;

:: deftheorem Def2 defines is_min_depend PARTIT1:def_2_:_
 for Y being non empty set
for PA, PB being a_partition of Y
for b being set holds
( b is_min_depend PA,PB iff ( b is_a_dependent_set_of PA & b is_a_dependent_set_of PB & ( for d being set st d c= b & d is_a_dependent_set_of PA & d is_a_dependent_set_of PB holds
d = b ) ) );

theorem Th6: :: PARTIT1:6
for Y being non empty set
for PA, PB being a_partition of Y st PA '>' PB holds
for b being set st b in PA holds
b is_a_dependent_set_of PB
proof
let Y be non empty set ; ::_thesis: for PA, PB being a_partition of Y st PA '>' PB holds
for b being set st b in PA holds
b is_a_dependent_set_of PB
let PA, PB be a_partition of Y; ::_thesis: ( PA '>' PB implies for b being set st b in PA holds
b is_a_dependent_set_of PB )
assume A1: PA '>' PB ; ::_thesis: for b being set st b in PA holds
b is_a_dependent_set_of PB
A2: union PB = Y by EQREL_1:def_4;
A3: PA is_coarser_than PB by A1, Th5;
 for b being set st b in PA holds
b is_a_dependent_set_of PB
proof
let b be set ; ::_thesis: ( b in PA implies b is_a_dependent_set_of PB )
assume A4: b in PA ; ::_thesis: b is_a_dependent_set_of PB
set B0 =  {  x8 where x8 is Subset of Y : ( x8 in PB & x8 c= b )  }  ;
consider xb being set  such that
A5: ( xb in PB & xb c= b ) by A3, A4, SETFAM_1:def_3;
A6: xb in  {  x8 where x8 is Subset of Y : ( x8 in PB & x8 c= b )  }  by A5;
 for z being set st z in  {  x8 where x8 is Subset of Y : ( x8 in PB & x8 c= b )  }  holds
z in PB
proof
let z be set ; ::_thesis: ( z in  {  x8 where x8 is Subset of Y : ( x8 in PB & x8 c= b )  }  implies z in PB )
assume  z in  {  x8 where x8 is Subset of Y : ( x8 in PB & x8 c= b )  }  ; ::_thesis: z in PB
then  ex x8 being Subset of Y st
( x8 = z & x8 in PB & x8 c= b ) ;
hence  z in PB ; ::_thesis: verum
end;
then A7:  {  x8 where x8 is Subset of Y : ( x8 in PB & x8 c= b )  }  c= PB by TARSKI:def_3;
 for z being set st z in b holds
z in union  {  x8 where x8 is Subset of Y : ( x8 in PB & x8 c= b )  }
proof
let z be set ; ::_thesis: ( z in b implies z in union  {  x8 where x8 is Subset of Y : ( x8 in PB & x8 c= b )  }  )
assume A8: z in b ; ::_thesis: z in union  {  x8 where x8 is Subset of Y : ( x8 in PB & x8 c= b )  }
then consider x1 being set  such that
A9: z in x1 and
A10: x1 in PB by A2, A4, TARSKI:def_4;
consider y1 being set  such that
A11: y1 in PA and
A12: x1 c= y1 by A1, A10, SETFAM_1:def_2;
 ( b = y1 or b misses y1 ) by A4, A11, EQREL_1:def_4;
then  x1 in  {  x8 where x8 is Subset of Y : ( x8 in PB & x8 c= b )  }  by A8, A9, A10, A12, XBOOLE_0:3;
hence  z in union  {  x8 where x8 is Subset of Y : ( x8 in PB & x8 c= b )  }  by A9, TARSKI:def_4; ::_thesis: verum
end;
then A13: b c= union  {  x8 where x8 is Subset of Y : ( x8 in PB & x8 c= b )  }  by TARSKI:def_3;
 for z being set st z in union  {  x8 where x8 is Subset of Y : ( x8 in PB & x8 c= b )  }  holds
z in b
proof
let z be set ; ::_thesis: ( z in union  {  x8 where x8 is Subset of Y : ( x8 in PB & x8 c= b )  }  implies z in b )
assume  z in union  {  x8 where x8 is Subset of Y : ( x8 in PB & x8 c= b )  }  ; ::_thesis: z in b
then consider y being set  such that
A14: z in y and
A15: y in  {  x8 where x8 is Subset of Y : ( x8 in PB & x8 c= b )  }  by TARSKI:def_4;
 ex x8 being Subset of Y st
( x8 = y & x8 in PB & x8 c= b ) by A15;
hence  z in b by A14; ::_thesis: verum
end;
then  union  {  x8 where x8 is Subset of Y : ( x8 in PB & x8 c= b )  }  c= b by TARSKI:def_3;
then  b = union  {  x8 where x8 is Subset of Y : ( x8 in PB & x8 c= b )  }  by A13, XBOOLE_0:def_10;
hence  b is_a_dependent_set_of PB by A6, A7, Def1; ::_thesis: verum
end;
hence  for b being set st b in PA holds
b is_a_dependent_set_of PB ; ::_thesis: verum
end;

theorem Th7: :: PARTIT1:7
for Y being non empty set
for PA being a_partition of Y holds Y is_a_dependent_set_of PA
proof
let Y be non empty set ; ::_thesis: for PA being a_partition of Y holds Y is_a_dependent_set_of PA
let PA be a_partition of Y; ::_thesis: Y is_a_dependent_set_of PA
A1: {Y} is Subset-Family of Y by ZFMISC_1:68;
A2: union {Y} = Y by ZFMISC_1:25;
 for A being Subset of Y st A in {Y} holds
( A <> {} & ( for B being Subset of Y holds
( not B in {Y} or A = B or A misses B ) ) )
proof
let A be Subset of Y; ::_thesis: ( A in {Y} implies ( A <> {} & ( for B being Subset of Y holds
( not B in {Y} or A = B or A misses B ) ) ) )
assume A3: A in {Y} ; ::_thesis: ( A <> {} & ( for B being Subset of Y holds
( not B in {Y} or A = B or A misses B ) ) )
then A4: A = Y by TARSKI:def_1;
thus  A <> {} by A3, TARSKI:def_1; ::_thesis: for B being Subset of Y holds
( not B in {Y} or A = B or A misses B )
let B be Subset of Y; ::_thesis: ( not B in {Y} or A = B or A misses B )
assume  B in {Y} ; ::_thesis: ( A = B or A misses B )
hence  ( A = B or A misses B ) by A4, TARSKI:def_1; ::_thesis: verum
end;
then A5: {Y} is a_partition of Y by A1, A2, EQREL_1:def_4;
 for a being set st a in PA holds
ex b being set st
( b in {Y} & a c= b )
proof
let a be set ; ::_thesis: ( a in PA implies ex b being set st
( b in {Y} & a c= b ) )
assume A6: a in PA ; ::_thesis: ex b being set st
( b in {Y} & a c= b )
then A7: a <> {} by EQREL_1:def_4;
set x = the Element of a;
 the Element of a in Y by A6, A7, TARSKI:def_3;
then consider b being set  such that
 the Element of a in b and
A8: b in {Y} by A2, TARSKI:def_4;
 b = Y by A8, TARSKI:def_1;
hence  ex b being set st
( b in {Y} & a c= b ) by A6, A8; ::_thesis: verum
end;
then A9: {Y} '>' PA by SETFAM_1:def_2;
 Y in {Y} by TARSKI:def_1;
hence  Y is_a_dependent_set_of PA by A5, A9, Th6; ::_thesis: verum
end;

theorem Th8: :: PARTIT1:8
for Y being non empty set
for PA being a_partition of Y
for F being Subset-Family of Y st Intersect F <> {} & ( for X being set st X in F holds
X is_a_dependent_set_of PA ) holds
Intersect F is_a_dependent_set_of PA
proof
let Y be non empty set ; ::_thesis: for PA being a_partition of Y
for F being Subset-Family of Y st Intersect F <> {} & ( for X being set st X in F holds
X is_a_dependent_set_of PA ) holds
Intersect F is_a_dependent_set_of PA
let PA be a_partition of Y; ::_thesis: for F being Subset-Family of Y st Intersect F <> {} & ( for X being set st X in F holds
X is_a_dependent_set_of PA ) holds
Intersect F is_a_dependent_set_of PA
let F be Subset-Family of Y; ::_thesis: ( Intersect F <> {} & ( for X being set st X in F holds
X is_a_dependent_set_of PA ) implies Intersect F is_a_dependent_set_of PA )
percases ( F = {} or F <> {} ) ;
suppose F = {} ; ::_thesis: ( Intersect F <> {} & ( for X being set st X in F holds
X is_a_dependent_set_of PA ) implies Intersect F is_a_dependent_set_of PA )
then  Intersect F = Y by SETFAM_1:def_9;
hence  ( Intersect F <> {} & ( for X being set st X in F holds
X is_a_dependent_set_of PA ) implies Intersect F is_a_dependent_set_of PA ) by Th7; ::_thesis: verum
end;
supposeA1: F <> {} ; ::_thesis: ( Intersect F <> {} & ( for X being set st X in F holds
X is_a_dependent_set_of PA ) implies Intersect F is_a_dependent_set_of PA )
then reconsider F9 = F as non empty Subset-Family of Y ;
assume that
A2: Intersect F <> {} and
A3: for X being set st X in F holds
X is_a_dependent_set_of PA ; ::_thesis: Intersect F is_a_dependent_set_of PA
defpred S1[ set , set ] means ( $2 c= PA & $2 <> {} & $1 = union $2 );
A4: for X being set st X in F holds
ex B being set st S1[X,B]
proof
let X be set ; ::_thesis: ( X in F implies ex B being set st S1[X,B] )
assume  X in F ; ::_thesis: ex B being set st S1[X,B]
then  X is_a_dependent_set_of PA by A3;
hence  ex B being set st S1[X,B] by Def1; ::_thesis: verum
end;
consider f being Function such that
A5: ( dom f = F & ( for X being set st X in F holds
S1[X,f . X] ) ) from CLASSES1:sch_1(A4);
 rng f c= bool (bool Y)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in bool (bool Y) )
assume  y in rng f ; ::_thesis: y in bool (bool Y)
then consider x being set  such that
A6: x in dom f and
A7: y = f . x by FUNCT_1:def_3;
 f . x c= PA by A5, A6;
then  y c= bool Y by A7, XBOOLE_1:1;
hence  y in bool (bool Y) ; ::_thesis: verum
end;
then reconsider f = f as Function of F9,(bool (bool Y)) by A5, FUNCT_2:def_1, RELSET_1:4;
defpred S2[ set ] means $1 in F;
deffunc H1( Element of F9) ->  Element of bool (bool Y) = f . $1;
reconsider T =  {  H1(X) where X is Element of F9 : S2[X]  }  as Subset-Family of (bool Y) from DOMAIN_1:sch_8();
reconsider T = T as Subset-Family of (bool Y) ;
take B = Intersect T; :: according to PARTIT1:def_1 ::_thesis: ( B c= PA & B <> {} & Intersect F = union B )
thus  B c= PA ::_thesis: ( B <> {} & Intersect F = union B )
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B or x in PA )
assume A8: x in B ; ::_thesis: x in PA
consider X being set  such that
A9: X in F by A1, XBOOLE_0:def_1;
 f . X in T by A9;
then A10: x in f . X by A8, SETFAM_1:43;
 f . X c= PA by A5, A9;
hence  x in PA by A10; ::_thesis: verum
end;
thus  B <> {} ::_thesis: Intersect F = union B
proof
consider X being set  such that
A11: X in F by A1, XBOOLE_0:def_1;
A12: f . X in T by A11;
consider A being set  such that
A13: A in Intersect F by A2, XBOOLE_0:def_1;
reconsider A = A as Element of Y by A13;
set AA = EqClass (A,PA);
A14: A in meet F by A1, A13, SETFAM_1:def_9;
 for X being set st X in T holds
EqClass (A,PA) in X
proof
let X be set ; ::_thesis: ( X in T implies EqClass (A,PA) in X )
assume  X in T ; ::_thesis: EqClass (A,PA) in X
then consider z being Element of F9 such that
A15: X = f . z and
 z in F ;
A16: f . z c= PA by A5;
 ( z = union (f . z) & A in z ) by A5, A14, SETFAM_1:def_1;
then  ex A0 being set st
( A in A0 & A0 in f . z ) by TARSKI:def_4;
hence  EqClass (A,PA) in X by A15, A16, EQREL_1:def_6; ::_thesis: verum
end;
then  EqClass (A,PA) in meet T by A12, SETFAM_1:def_1;
hence  B <> {} by SETFAM_1:def_9; ::_thesis: verum
end;
A17: Intersect F c= union B
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Intersect F or x in union B )
assume A18: x in Intersect F ; ::_thesis: x in union B
then A19: x in meet F by A1, SETFAM_1:def_9;
reconsider x = x as Element of Y by A18;
reconsider PA = PA as a_partition of Y ;
set A = EqClass (x,PA);
consider X being set  such that
A20: X in F by A1, XBOOLE_0:def_1;
A21: f . X in T by A20;
 for X being set st X in T holds
EqClass (x,PA) in X
proof
let X be set ; ::_thesis: ( X in T implies EqClass (x,PA) in X )
assume  X in T ; ::_thesis: EqClass (x,PA) in X
then consider z being Element of F9 such that
A22: X = f . z and
 z in F ;
A23: f . z c= PA by A5;
 z = union (f . z) by A5;
then  x in union (f . z) by A19, SETFAM_1:def_1;
then  ex A0 being set st
( x in A0 & A0 in f . z ) by TARSKI:def_4;
hence  EqClass (x,PA) in X by A22, A23, EQREL_1:def_6; ::_thesis: verum
end;
then  EqClass (x,PA) in meet T by A21, SETFAM_1:def_1;
then  ( x in EqClass (x,PA) & EqClass (x,PA) in Intersect T ) by A21, EQREL_1:def_6, SETFAM_1:def_9;
hence  x in union B by TARSKI:def_4; ::_thesis: verum
end;
 union B c= Intersect F
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union B or x in Intersect F )
assume A24: x in union B ; ::_thesis: x in Intersect F
consider X being set  such that
A25: X in F by A1, XBOOLE_0:def_1;
A26: f . X in T by A25;
consider y being set  such that
A27: x in y and
A28: y in B by A24, TARSKI:def_4;
A29: y in meet T by A26, A28, SETFAM_1:def_9;
 for X being set st X in F holds
x in X
proof
let X be set ; ::_thesis: ( X in F implies x in X )
assume A30: X in F ; ::_thesis: x in X
then  f . X in T ;
then A31: y in f . X by A29, SETFAM_1:def_1;
 X = union (f . X) by A5, A30;
hence  x in X by A27, A31, TARSKI:def_4; ::_thesis: verum
end;
then  x in meet F by A1, SETFAM_1:def_1;
hence  x in Intersect F by A1, SETFAM_1:def_9; ::_thesis: verum
end;
hence  Intersect F = union B by A17, XBOOLE_0:def_10; ::_thesis: verum
end;
end;
end;

theorem Th9: :: PARTIT1:9
for Y being non empty set
for PA being a_partition of Y
for X0, X1 being Subset of Y st X0 is_a_dependent_set_of PA & X1 is_a_dependent_set_of PA & X0 meets X1 holds
X0 /\ X1 is_a_dependent_set_of PA
proof
let Y be non empty set ; ::_thesis: for PA being a_partition of Y
for X0, X1 being Subset of Y st X0 is_a_dependent_set_of PA & X1 is_a_dependent_set_of PA & X0 meets X1 holds
X0 /\ X1 is_a_dependent_set_of PA
let PA be a_partition of Y; ::_thesis: for X0, X1 being Subset of Y st X0 is_a_dependent_set_of PA & X1 is_a_dependent_set_of PA & X0 meets X1 holds
X0 /\ X1 is_a_dependent_set_of PA
let X0, X1 be Subset of Y; ::_thesis: ( X0 is_a_dependent_set_of PA & X1 is_a_dependent_set_of PA & X0 meets X1 implies X0 /\ X1 is_a_dependent_set_of PA )
assume that
A1: X0 is_a_dependent_set_of PA and
A2: X1 is_a_dependent_set_of PA and
A3: X0 meets X1 ; ::_thesis: X0 /\ X1 is_a_dependent_set_of PA
consider A being set  such that
A4: A c= PA and
 A <> {} and
A5: X0 = union A by A1, Def1;
consider B being set  such that
A6: B c= PA and
 B <> {} and
A7: X1 = union B by A2, Def1;
A8: X0 /\ X1 c= union (A /\ B)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X0 /\ X1 or x in union (A /\ B) )
assume A9: x in X0 /\ X1 ; ::_thesis: x in union (A /\ B)
then A10: x in X0 by XBOOLE_0:def_4;
A11: x in X1 by A9, XBOOLE_0:def_4;
consider y being set  such that
A12: x in y and
A13: y in A by A5, A10, TARSKI:def_4;
consider z being set  such that
A14: x in z and
A15: z in B by A7, A11, TARSKI:def_4;
A16: y in PA by A4, A13;
A17: z in PA by A6, A15;
 y meets z by A12, A14, XBOOLE_0:3;
then  y = z by A16, A17, EQREL_1:def_4;
then  y in A /\ B by A13, A15, XBOOLE_0:def_4;
hence  x in union (A /\ B) by A12, TARSKI:def_4; ::_thesis: verum
end;
 union (A /\ B) c= X0 /\ X1
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union (A /\ B) or x in X0 /\ X1 )
assume  x in union (A /\ B) ; ::_thesis: x in X0 /\ X1
then consider y being set  such that
A18: x in y and
A19: y in A /\ B by TARSKI:def_4;
A20: y in A by A19, XBOOLE_0:def_4;
A21: y in B by A19, XBOOLE_0:def_4;
A22: x in X0 by A5, A18, A20, TARSKI:def_4;
 x in X1 by A7, A18, A21, TARSKI:def_4;
hence  x in X0 /\ X1 by A22, XBOOLE_0:def_4; ::_thesis: verum
end;
then A23: X0 /\ X1 = union (A /\ B) by A8, XBOOLE_0:def_10;
A24: A \/ B c= PA by A4, A6, XBOOLE_1:8;
 ( A /\ B c= A & A c= A \/ B ) by XBOOLE_1:7, XBOOLE_1:17;
then  A /\ B c= A \/ B by XBOOLE_1:1;
then A25: A /\ B c= PA by A24, XBOOLE_1:1;
now__::_thesis:_not_A_/\_B_=_{}
assume A26: A /\ B = {} ; ::_thesis: contradiction
 ex y being set st
( y in X0 & y in X1 ) by A3, XBOOLE_0:3;
hence  contradiction by A8, A26, XBOOLE_0:def_4, ZFMISC_1:2; ::_thesis: verum
end;
hence  X0 /\ X1 is_a_dependent_set_of PA by A23, A25, Def1; ::_thesis: verum
end;

theorem Th10: :: PARTIT1:10
for Y being non empty set
for PA being a_partition of Y
for X being Subset of Y st X is_a_dependent_set_of PA & X <> Y holds
X ` is_a_dependent_set_of PA
proof
let Y be non empty set ; ::_thesis: for PA being a_partition of Y
for X being Subset of Y st X is_a_dependent_set_of PA & X <> Y holds
X ` is_a_dependent_set_of PA
let PA be a_partition of Y; ::_thesis: for X being Subset of Y st X is_a_dependent_set_of PA & X <> Y holds
X ` is_a_dependent_set_of PA
let X be Subset of Y; ::_thesis: ( X is_a_dependent_set_of PA & X <> Y implies X ` is_a_dependent_set_of PA )
assume that
A1: X is_a_dependent_set_of PA and
A2: X <> Y ; ::_thesis: X ` is_a_dependent_set_of PA
consider B being set  such that
A3: B c= PA and
 B <> {} and
A4: X = union B by A1, Def1;
take  PA \ B ; :: according to PARTIT1:def_1 ::_thesis: ( PA \ B c= PA & PA \ B <> {} & X ` = union (PA \ B) )
A5: union PA = Y by EQREL_1:def_4;
then A6: X ` = (union PA) \ (union B) by A4, SUBSET_1:def_4;
reconsider B = B as Subset of PA by A3;
now__::_thesis:_not_PA_\_B_=_{}
assume  PA \ B = {} ; ::_thesis: contradiction
then  PA c= B by XBOOLE_1:37;
hence  contradiction by A2, A4, A5, XBOOLE_0:def_10; ::_thesis: verum
end;
hence  ( PA \ B c= PA & PA \ B <> {} & X ` = union (PA \ B) ) by A6, EQREL_1:43, XBOOLE_1:36; ::_thesis: verum
end;

theorem Th11: :: PARTIT1:11
for Y being non empty set
for PA, PB being a_partition of Y
for y being Element of Y ex X being Subset of Y st
( y in X & X is_min_depend PA,PB )
proof
let Y be non empty set ; ::_thesis: for PA, PB being a_partition of Y
for y being Element of Y ex X being Subset of Y st
( y in X & X is_min_depend PA,PB )
let PA, PB be a_partition of Y; ::_thesis: for y being Element of Y ex X being Subset of Y st
( y in X & X is_min_depend PA,PB )
let y be Element of Y; ::_thesis: ex X being Subset of Y st
( y in X & X is_min_depend PA,PB )
A1: union PA = Y by EQREL_1:def_4;
A2: for A being set st A in PA holds
( A <> {} & ( for B being set holds
( not B in PA or A = B or A misses B ) ) ) by EQREL_1:def_4;
A3: ( Y is_a_dependent_set_of PA & Y is_a_dependent_set_of PB ) by Th7;
defpred S1[ set ] means ( y in $1 & $1 is_a_dependent_set_of PA & $1 is_a_dependent_set_of PB );
reconsider XX =  {  X where X is Subset of Y : S1[X]  }  as Subset-Family of Y from DOMAIN_1:sch_7();
reconsider XX = XX as Subset-Family of Y ;
 Y c= Y ;
then A4: Y in XX by A3;
 for X1 being set st X1 in XX holds
y in X1
proof
let X1 be set ; ::_thesis: ( X1 in XX implies y in X1 )
assume  X1 in XX ; ::_thesis: y in X1
then  ex X being Subset of Y st
( X = X1 & y in X & X is_a_dependent_set_of PA & X is_a_dependent_set_of PB ) ;
hence  y in X1 ; ::_thesis: verum
end;
then A5: y in meet XX by A4, SETFAM_1:def_1;
then A6: Intersect XX <> {} by SETFAM_1:def_9;
take  Intersect XX ; ::_thesis: ( y in Intersect XX & Intersect XX is_min_depend PA,PB )
 for X1 being set st X1 in XX holds
X1 is_a_dependent_set_of PA
proof
let X1 be set ; ::_thesis: ( X1 in XX implies X1 is_a_dependent_set_of PA )
assume  X1 in XX ; ::_thesis: X1 is_a_dependent_set_of PA
then  ex X being Subset of Y st
( X = X1 & y in X & X is_a_dependent_set_of PA & X is_a_dependent_set_of PB ) ;
hence  X1 is_a_dependent_set_of PA ; ::_thesis: verum
end;
then A7: Intersect XX is_a_dependent_set_of PA by A6, Th8;
 for X1 being set st X1 in XX holds
X1 is_a_dependent_set_of PB
proof
let X1 be set ; ::_thesis: ( X1 in XX implies X1 is_a_dependent_set_of PB )
assume  X1 in XX ; ::_thesis: X1 is_a_dependent_set_of PB
then  ex X being Subset of Y st
( X = X1 & y in X & X is_a_dependent_set_of PA & X is_a_dependent_set_of PB ) ;
hence  X1 is_a_dependent_set_of PB ; ::_thesis: verum
end;
then A8: Intersect XX is_a_dependent_set_of PB by A6, Th8;
 for d being set st d c= Intersect XX & d is_a_dependent_set_of PA & d is_a_dependent_set_of PB holds
d = Intersect XX
proof
let d be set ; ::_thesis: ( d c= Intersect XX & d is_a_dependent_set_of PA & d is_a_dependent_set_of PB implies d = Intersect XX )
assume that
A9: d c= Intersect XX and
A10: d is_a_dependent_set_of PA and
A11: d is_a_dependent_set_of PB ; ::_thesis: d = Intersect XX
consider Ad being set  such that
A12: Ad c= PA and
A13: Ad <> {} and
A14: d = union Ad by A10, Def1;
A15: d c= Y by A1, A12, A14, ZFMISC_1:77;
percases ( y in d or not y in d ) ;
suppose y in d ; ::_thesis: d = Intersect XX
then A16: d in XX by A10, A11, A15;
 Intersect XX c= d
proof
let X1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not X1 in Intersect XX or X1 in d )
assume  X1 in Intersect XX ; ::_thesis: X1 in d
then  X1 in meet XX by A4, SETFAM_1:def_9;
hence  X1 in d by A16, SETFAM_1:def_1; ::_thesis: verum
end;
hence  d = Intersect XX by A9, XBOOLE_0:def_10; ::_thesis: verum
end;
supposeA17: not y in d ; ::_thesis: d = Intersect XX
reconsider d = d as Subset of Y by A1, A12, A14, ZFMISC_1:77;
 d ` = Y \ d by SUBSET_1:def_4;
then A18: y in d ` by A17, XBOOLE_0:def_5;
 d misses d ` by SUBSET_1:24;
then A19: d /\ (d `) = {} by XBOOLE_0:def_7;
 d <> Y by A17;
then  ( d ` is_a_dependent_set_of PA & d ` is_a_dependent_set_of PB ) by A10, A11, Th10;
then A20: d ` in XX by A18;
 Intersect XX c= d `
proof
let X1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not X1 in Intersect XX or X1 in d ` )
assume  X1 in Intersect XX ; ::_thesis: X1 in d `
then  X1 in meet XX by A4, SETFAM_1:def_9;
hence  X1 in d ` by A20, SETFAM_1:def_1; ::_thesis: verum
end;
then A21: d /\ (Intersect XX) = {} by A19, XBOOLE_1:3, XBOOLE_1:26;
 d /\ d c= d /\ (Intersect XX) by A9, XBOOLE_1:26;
then A22: union Ad = {} by A14, A21;
consider ad being set  such that
A23: ad in Ad by A13, XBOOLE_0:def_1;
A24: ad <> {} by A2, A12, A23;
 ad c= {} by A22, A23, ZFMISC_1:74;
hence  d = Intersect XX by A24; ::_thesis: verum
end;
end;
end;
hence  ( y in Intersect XX & Intersect XX is_min_depend PA,PB ) by A4, A5, A7, A8, Def2, SETFAM_1:def_9; ::_thesis: verum
end;

theorem :: PARTIT1:12
for Y being non empty set
for P being a_partition of Y
for y being Element of Y ex A being Subset of Y st
( y in A & A in P )
proof
let Y be non empty set ; ::_thesis: for P being a_partition of Y
for y being Element of Y ex A being Subset of Y st
( y in A & A in P )
let P be a_partition of Y; ::_thesis: for y being Element of Y ex A being Subset of Y st
( y in A & A in P )
let y be Element of Y; ::_thesis: ex A being Subset of Y st
( y in A & A in P )
consider R being Equivalence_Relation of Y such that
A1: P = Class R by EQREL_1:34;
take  Class (R,y) ; ::_thesis: ( y in Class (R,y) & Class (R,y) in P )
thus  y in Class (R,y) by EQREL_1:20; ::_thesis: Class (R,y) in P
thus  Class (R,y) in P by A1, EQREL_1:def_3; ::_thesis: verum
end;

definition
let Y be set ;
func PARTITIONS Y ->  set  means :Def3: :: PARTIT1:def 3
 for x being set holds
( x in it iff x is a_partition of Y );
existence
 ex b1 being set st
for x being set holds
( x in b1 iff x is a_partition of Y )
proof
defpred S1[ set ] means $1 is a_partition of Y;
consider X being set  such that
A1: for x being set holds
( x in X iff ( x in bool (bool Y) & S1[x] ) ) from XBOOLE_0:sch_1();
take  X ; ::_thesis: for x being set holds
( x in X iff x is a_partition of Y )
let x be set ; ::_thesis: ( x in X iff x is a_partition of Y )
thus  ( x in X implies x is a_partition of Y ) by A1; ::_thesis: ( x is a_partition of Y implies x in X )
assume  x is a_partition of Y ; ::_thesis: x in X
hence  x in X by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff x is a_partition of Y ) ) & ( for x being set holds
( x in b2 iff x is a_partition of Y ) ) holds
b1 = b2
proof
let A1, A2 be set ; ::_thesis: ( ( for x being set holds
( x in A1 iff x is a_partition of Y ) ) & ( for x being set holds
( x in A2 iff x is a_partition of Y ) ) implies A1 = A2 )
assume that
A2: for x being set holds
( x in A1 iff x is a_partition of Y ) and
A3: for x being set holds
( x in A2 iff x is a_partition of Y ) ; ::_thesis: A1 = A2
now__::_thesis:_for_y_being_set_holds_
(_y_in_A1_iff_y_in_A2_)
let y be set ; ::_thesis: ( y in A1 iff y in A2 )
 ( y in A1 iff y is a_partition of Y ) by A2;
hence  ( y in A1 iff y in A2 ) by A3; ::_thesis: verum
end;
hence  A1 = A2 by TARSKI:1; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines PARTITIONS PARTIT1:def_3_:_
 for Y being set
for b2 being set holds
( b2 = PARTITIONS Y iff for x being set holds
( x in b2 iff x is a_partition of Y ) );

registration
let Y be set ;
cluster PARTITIONS Y ->  non empty ;
coherence
 not PARTITIONS Y is empty
proof
percases ( Y = {} or Y <> {} ) ;
suppose Y = {} ; ::_thesis: not PARTITIONS Y is empty
hence  not PARTITIONS Y is empty by Def3, EQREL_1:45; ::_thesis: verum
end;
suppose Y <> {} ; ::_thesis: not PARTITIONS Y is empty
then reconsider Y = Y as non empty set ;
A1: ( {Y} is Subset-Family of Y & union {Y} = Y ) by ZFMISC_1:25, ZFMISC_1:68;
 for A being Subset of Y st A in {Y} holds
( A <> {} & ( for B being Subset of Y holds
( not B in {Y} or A = B or A misses B ) ) )
proof
let A be Subset of Y; ::_thesis: ( A in {Y} implies ( A <> {} & ( for B being Subset of Y holds
( not B in {Y} or A = B or A misses B ) ) ) )
assume A2: A in {Y} ; ::_thesis: ( A <> {} & ( for B being Subset of Y holds
( not B in {Y} or A = B or A misses B ) ) )
then A3: A = Y by TARSKI:def_1;
thus  A <> {} by A2, TARSKI:def_1; ::_thesis: for B being Subset of Y holds
( not B in {Y} or A = B or A misses B )
let B be Subset of Y; ::_thesis: ( not B in {Y} or A = B or A misses B )
assume  B in {Y} ; ::_thesis: ( A = B or A misses B )
hence  ( A = B or A misses B ) by A3, TARSKI:def_1; ::_thesis: verum
end;
then  {Y} is a_partition of Y by A1, EQREL_1:def_4;
hence  not PARTITIONS Y is empty by Def3; ::_thesis: verum
end;
end;
end;
end;

begin

definition
let Y be non empty set ;
let PA, PB be a_partition of Y;
funcPA '/\' PB ->  a_partition of Y equals :: PARTIT1:def 4
(INTERSECTION (PA,PB)) \ {{}};
correctness
coherence
(INTERSECTION (PA,PB)) \ {{}} is a_partition of Y;
proof
 {} c= Y by XBOOLE_1:2;
then reconsider e = {{}} as Subset-Family of Y by ZFMISC_1:31;
set a = INTERSECTION (PA,PB);
 for z being set st z in INTERSECTION (PA,PB) holds
z in bool Y
proof
let z be set ; ::_thesis: ( z in INTERSECTION (PA,PB) implies z in bool Y )
assume  z in INTERSECTION (PA,PB) ; ::_thesis: z in bool Y
then  ex M, N being set st
( M in PA & N in PB & z = M /\ N ) by SETFAM_1:def_5;
then  z c= Y by XBOOLE_1:108;
hence  z in bool Y ; ::_thesis: verum
end;
then reconsider a = INTERSECTION (PA,PB) as Subset-Family of Y by TARSKI:def_3;
reconsider ia = a \ e as Subset-Family of Y ;
A1: ( union PA = Y & union PB = Y ) by EQREL_1:def_4;
A2: union ia = union (INTERSECTION (PA,PB)) by Th2
.= (union PA) /\ (union PB) by SETFAM_1:28
.= Y by A1 ;
 for A being Subset of Y st A in ia holds
( A <> {} & ( for B being Subset of Y holds
( not B in ia or A = B or A misses B ) ) )
proof
let A be Subset of Y; ::_thesis: ( A in ia implies ( A <> {} & ( for B being Subset of Y holds
( not B in ia or A = B or A misses B ) ) ) )
assume A3: A in ia ; ::_thesis: ( A <> {} & ( for B being Subset of Y holds
( not B in ia or A = B or A misses B ) ) )
then A4: not A in {{}} by XBOOLE_0:def_5;
A5: A in INTERSECTION (PA,PB) by A3, XBOOLE_0:def_5;
 for B being Subset of Y holds
( not B in ia or A = B or A misses B )
proof
A6: for m, n, o, p being set holds (m /\ n) /\ (o /\ p) = m /\ ((n /\ o) /\ p)
proof
let m, n, o, p be set ; ::_thesis: (m /\ n) /\ (o /\ p) = m /\ ((n /\ o) /\ p)
(m /\ n) /\ (o /\ p) = m /\ (n /\ (o /\ p)) by XBOOLE_1:16
.= m /\ ((n /\ o) /\ p) by XBOOLE_1:16 ;
hence  (m /\ n) /\ (o /\ p) = m /\ ((n /\ o) /\ p) ; ::_thesis: verum
end;
let B be Subset of Y; ::_thesis: ( not B in ia or A = B or A misses B )
assume  B in ia ; ::_thesis: ( A = B or A misses B )
then  B in INTERSECTION (PA,PB) by XBOOLE_0:def_5;
then consider M, N being set  such that
A7: ( M in PA & N in PB ) and
A8: B = M /\ N by SETFAM_1:def_5;
consider S, T being set  such that
A9: ( S in PA & T in PB ) and
A10: A = S /\ T by A5, SETFAM_1:def_5;
 ( M /\ N = S /\ T or not M = S or not N = T ) ;
then  ( M /\ N = S /\ T or M misses S or N misses T ) by A7, A9, EQREL_1:def_4;
then A11: ( M /\ N = S /\ T or M /\ S = {} or N /\ T = {} ) by XBOOLE_0:def_7;
(M /\ S) /\ (N /\ T) = M /\ ((S /\ N) /\ T) by A6
.= (M /\ N) /\ (S /\ T) by A6 ;
hence  ( A = B or A misses B ) by A8, A10, A11, XBOOLE_0:def_7; ::_thesis: verum
end;
hence  ( A <> {} & ( for B being Subset of Y holds
( not B in ia or A = B or A misses B ) ) ) by A4, TARSKI:def_1; ::_thesis: verum
end;
hence  (INTERSECTION (PA,PB)) \ {{}} is a_partition of Y by A2, EQREL_1:def_4; ::_thesis: verum
end;
commutativity
 for b1, PA, PB being a_partition of Y st b1 = (INTERSECTION (PA,PB)) \ {{}} holds
b1 = (INTERSECTION (PB,PA)) \ {{}} ;
end;

:: deftheorem  defines '/\' PARTIT1:def_4_:_
 for Y being non empty set
for PA, PB being a_partition of Y holds PA '/\' PB = (INTERSECTION (PA,PB)) \ {{}};

theorem :: PARTIT1:13
for Y being non empty set
for PA being a_partition of Y holds PA '/\' PA = PA
proof
let Y be non empty set ; ::_thesis: for PA being a_partition of Y holds PA '/\' PA = PA
let PA be a_partition of Y; ::_thesis: PA '/\' PA = PA
 for u being set st u in (INTERSECTION (PA,PA)) \ {{}} holds
ex v being set st
( v in PA & u c= v )
proof
let u be set ; ::_thesis: ( u in (INTERSECTION (PA,PA)) \ {{}} implies ex v being set st
( v in PA & u c= v ) )
assume  u in (INTERSECTION (PA,PA)) \ {{}} ; ::_thesis: ex v being set st
( v in PA & u c= v )
then consider v, u2 being set  such that
A1: v in PA and
 u2 in PA and
A2: u = v /\ u2 by SETFAM_1:def_5;
take  v ; ::_thesis: ( v in PA & u c= v )
thus  ( v in PA & u c= v ) by A1, A2, XBOOLE_1:17; ::_thesis: verum
end;
then A3: (INTERSECTION (PA,PA)) \ {{}} '<' PA by SETFAM_1:def_2;
 for u being set st u in PA holds
ex v being set st
( v in (INTERSECTION (PA,PA)) \ {{}} & u c= v )
proof
let u be set ; ::_thesis: ( u in PA implies ex v being set st
( v in (INTERSECTION (PA,PA)) \ {{}} & u c= v ) )
assume A4: u in PA ; ::_thesis: ex v being set st
( v in (INTERSECTION (PA,PA)) \ {{}} & u c= v )
then A5: u <> {} by EQREL_1:def_4;
set v = u /\ u;
A6: not u /\ u in {{}} by A5, TARSKI:def_1;
 u /\ u in INTERSECTION (PA,PA) by A4, SETFAM_1:def_5;
then  u /\ u in (INTERSECTION (PA,PA)) \ {{}} by A6, XBOOLE_0:def_5;
hence  ex v being set st
( v in (INTERSECTION (PA,PA)) \ {{}} & u c= v ) ; ::_thesis: verum
end;
then  PA '<' (INTERSECTION (PA,PA)) \ {{}} by SETFAM_1:def_2;
hence  PA '/\' PA = PA by A3, Th4; ::_thesis: verum
end;

theorem :: PARTIT1:14
for Y being non empty set
for PA, PB, PC being a_partition of Y holds (PA '/\' PB) '/\' PC = PA '/\' (PB '/\' PC)
proof
let Y be non empty set ; ::_thesis: for PA, PB, PC being a_partition of Y holds (PA '/\' PB) '/\' PC = PA '/\' (PB '/\' PC)
let PA, PB, PC be a_partition of Y; ::_thesis: (PA '/\' PB) '/\' PC = PA '/\' (PB '/\' PC)
consider PD, PE being a_partition of Y such that
A1: PD = PA '/\' PB and
A2: PE = PB '/\' PC ;
 for u being set st u in PD '/\' PC holds
ex v being set st
( v in PA '/\' PE & u c= v )
proof
let u be set ; ::_thesis: ( u in PD '/\' PC implies ex v being set st
( v in PA '/\' PE & u c= v ) )
assume A3: u in PD '/\' PC ; ::_thesis: ex v being set st
( v in PA '/\' PE & u c= v )
then consider u1, u2 being set  such that
A4: u1 in PD and
A5: u2 in PC and
A6: u = u1 /\ u2 by SETFAM_1:def_5;
consider u3, u4 being set  such that
A7: u3 in PA and
A8: u4 in PB and
A9: u1 = u3 /\ u4 by A1, A4, SETFAM_1:def_5;
consider v, v1, v2 being set  such that
A10: v1 = u4 /\ u2 and
A11: v2 = u3 and
A12: v = (u3 /\ u4) /\ u2 ;
A13: v = v2 /\ v1 by A10, A11, A12, XBOOLE_1:16;
A14: v1 in INTERSECTION (PB,PC) by A5, A8, A10, SETFAM_1:def_5;
A15: not u in {{}} by A3, XBOOLE_0:def_5;
 u = u3 /\ v1 by A6, A9, A10, XBOOLE_1:16;
then  v1 <> {} by A15, TARSKI:def_1;
then  not v1 in {{}} by TARSKI:def_1;
then  v1 in (INTERSECTION (PB,PC)) \ {{}} by A14, XBOOLE_0:def_5;
then A16: v in INTERSECTION (PA,PE) by A2, A7, A11, A13, SETFAM_1:def_5;
take  v ; ::_thesis: ( v in PA '/\' PE & u c= v )
thus  ( v in PA '/\' PE & u c= v ) by A6, A9, A12, A15, A16, XBOOLE_0:def_5; ::_thesis: verum
end;
then A17: PD '/\' PC '<' PA '/\' PE by SETFAM_1:def_2;
 for u being set st u in PA '/\' PE holds
ex v being set st
( v in PD '/\' PC & u c= v )
proof
let u be set ; ::_thesis: ( u in PA '/\' PE implies ex v being set st
( v in PD '/\' PC & u c= v ) )
assume A18: u in PA '/\' PE ; ::_thesis: ex v being set st
( v in PD '/\' PC & u c= v )
then consider u1, u2 being set  such that
A19: u1 in PA and
A20: u2 in PE and
A21: u = u1 /\ u2 by SETFAM_1:def_5;
consider u3, u4 being set  such that
A22: u3 in PB and
A23: u4 in PC and
A24: u2 = u3 /\ u4 by A2, A20, SETFAM_1:def_5;
A25: u = (u1 /\ u3) /\ u4 by A21, A24, XBOOLE_1:16;
consider v, v1, v2 being set  such that
A26: v1 = u1 /\ u3 and
 v2 = u4 and
A27: v = (u1 /\ u3) /\ u4 ;
A28: v1 in INTERSECTION (PA,PB) by A19, A22, A26, SETFAM_1:def_5;
A29: not u in {{}} by A18, XBOOLE_0:def_5;
then  v1 <> {} by A25, A26, TARSKI:def_1;
then  not v1 in {{}} by TARSKI:def_1;
then  v1 in (INTERSECTION (PA,PB)) \ {{}} by A28, XBOOLE_0:def_5;
then A30: v in INTERSECTION (PD,PC) by A1, A23, A26, A27, SETFAM_1:def_5;
take  v ; ::_thesis: ( v in PD '/\' PC & u c= v )
thus  ( v in PD '/\' PC & u c= v ) by A25, A27, A29, A30, XBOOLE_0:def_5; ::_thesis: verum
end;
then  PA '/\' PE '<' PD '/\' PC by SETFAM_1:def_2;
hence  (PA '/\' PB) '/\' PC = PA '/\' (PB '/\' PC) by A1, A2, A17, Th4; ::_thesis: verum
end;

theorem Th15: :: PARTIT1:15
for Y being non empty set
for PA, PB being a_partition of Y holds PA '>' PA '/\' PB
proof
let Y be non empty set ; ::_thesis: for PA, PB being a_partition of Y holds PA '>' PA '/\' PB
let PA, PB be a_partition of Y; ::_thesis: PA '>' PA '/\' PB
 for u being set st u in PA '/\' PB holds
ex v being set st
( v in PA & u c= v )
proof
let u be set ; ::_thesis: ( u in PA '/\' PB implies ex v being set st
( v in PA & u c= v ) )
assume  u in PA '/\' PB ; ::_thesis: ex v being set st
( v in PA & u c= v )
then consider u1, u2 being set  such that
A1: u1 in PA and
 u2 in PB and
A2: u = u1 /\ u2 by SETFAM_1:def_5;
take  u1 ; ::_thesis: ( u1 in PA & u c= u1 )
thus  ( u1 in PA & u c= u1 ) by A1, A2, XBOOLE_1:17; ::_thesis: verum
end;
hence  PA '>' PA '/\' PB by SETFAM_1:def_2; ::_thesis: verum
end;

definition
let Y be non empty set ;
let PA, PB be a_partition of Y;
funcPA '\/' PB ->  a_partition of Y means :Def5: :: PARTIT1:def 5
 for d being set holds
( d in it iff d is_min_depend PA,PB );
existence
 ex b1 being a_partition of Y st
for d being set holds
( d in b1 iff d is_min_depend PA,PB )
proof
A1: union PA = Y by EQREL_1:def_4;
A2: for A being set st A in PA holds
( A <> {} & ( for B being set holds
( not B in PA or A = B or A misses B ) ) ) by EQREL_1:def_4;
defpred S1[ set ] means $1 is_min_depend PA,PB;
consider X being set  such that
A3: for d being set holds
( d in X iff ( d in bool Y & S1[d] ) ) from XBOOLE_0:sch_1();
A4: for d being set holds
( d in X iff d is_min_depend PA,PB )
proof
let d be set ; ::_thesis: ( d in X iff d is_min_depend PA,PB )
 for d being set st d is_min_depend PA,PB holds
d in bool Y
proof
let d be set ; ::_thesis: ( d is_min_depend PA,PB implies d in bool Y )
assume  d is_min_depend PA,PB ; ::_thesis: d in bool Y
then  d is_a_dependent_set_of PA by Def2;
then  ex A being set st
( A c= PA & A <> {} & d = union A ) by Def1;
then  d c= union PA by ZFMISC_1:77;
hence  d in bool Y by A1; ::_thesis: verum
end;
then  ( d is_min_depend PA,PB implies ( d is_min_depend PA,PB & d in bool Y ) ) ;
hence  ( d in X iff d is_min_depend PA,PB ) by A3; ::_thesis: verum
end;
take  X ; ::_thesis: ( X is Element of bool (bool Y) & X is a_partition of Y & ( for d being set holds
( d in X iff d is_min_depend PA,PB ) ) )
A5: Y c= union X
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Y or y in union X )
assume  y in Y ; ::_thesis: y in union X
then consider a being Subset of Y such that
A6: y in a and
A7: a is_min_depend PA,PB by Th11;
 a in X by A4, A7;
hence  y in union X by A6, TARSKI:def_4; ::_thesis: verum
end;
 union X c= Y
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in union X or y in Y )
assume  y in union X ; ::_thesis: y in Y
then consider a being set  such that
A8: y in a and
A9: a in X by TARSKI:def_4;
 a is_min_depend PA,PB by A4, A9;
then  a is_a_dependent_set_of PA by Def2;
then  ex A being set st
( A c= PA & A <> {} & a = union A ) by Def1;
then  a c= Y by A1, ZFMISC_1:77;
hence  y in Y by A8; ::_thesis: verum
end;
then A10: union X = Y by A5, XBOOLE_0:def_10;
A11: for A being Subset of Y st A in X holds
( A <> {} & ( for B being Subset of Y holds
( not B in X or A = B or A misses B ) ) )
proof
let A be Subset of Y; ::_thesis: ( A in X implies ( A <> {} & ( for B being Subset of Y holds
( not B in X or A = B or A misses B ) ) ) )
assume  A in X ; ::_thesis: ( A <> {} & ( for B being Subset of Y holds
( not B in X or A = B or A misses B ) ) )
then A12: A is_min_depend PA,PB by A4;
then A13: A is_a_dependent_set_of PA by Def2;
A14: A is_a_dependent_set_of PB by A12, Def2;
consider Aa being set  such that
A15: Aa c= PA and
A16: Aa <> {} and
A17: A = union Aa by A13, Def1;
consider aa being set  such that
A18: aa in Aa by A16, XBOOLE_0:def_1;
A19: aa <> {} by A2, A15, A18;
 aa c= union Aa by A18, ZFMISC_1:74;
hence  A <> {} by A17, A19; ::_thesis: for B being Subset of Y holds
( not B in X or A = B or A misses B )
let B be Subset of Y; ::_thesis: ( not B in X or A = B or A misses B )
assume  B in X ; ::_thesis: ( A = B or A misses B )
then A20: B is_min_depend PA,PB by A4;
then A21: ( B is_a_dependent_set_of PA & B is_a_dependent_set_of PB ) by Def2;
now__::_thesis:_(_A_meets_B_implies_A_=_B_)
assume  A meets B ; ::_thesis: A = B
then A22: ( A /\ B is_a_dependent_set_of PA & A /\ B is_a_dependent_set_of PB ) by A13, A14, A21, Th9;
 A /\ B c= A by XBOOLE_1:17;
then A23: A /\ B = A by A12, A22, Def2;
A24: A c= B
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in B )
assume  x in A ; ::_thesis: x in B
hence  x in B by A23, XBOOLE_0:def_4; ::_thesis: verum
end;
 A /\ B c= B by XBOOLE_1:17;
then A25: A /\ B = B by A20, A22, Def2;
 B c= A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B or x in A )
assume  x in B ; ::_thesis: x in A
hence  x in A by A25, XBOOLE_0:def_4; ::_thesis: verum
end;
hence  A = B by A24, XBOOLE_0:def_10; ::_thesis: verum
end;
hence  ( A = B or A misses B ) ; ::_thesis: verum
end;
 X c= bool Y
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in bool Y )
assume  x in X ; ::_thesis: x in bool Y
then  x is_min_depend PA,PB by A4;
then  x is_a_dependent_set_of PA by Def2;
then  ex a being set st
( a c= PA & a <> {} & x = union a ) by Def1;
then  x c= Y by A1, ZFMISC_1:77;
hence  x in bool Y ; ::_thesis: verum
end;
then reconsider X = X as Subset-Family of Y ;
 X is a_partition of Y by A10, A11, EQREL_1:def_4;
hence  ( X is Element of bool (bool Y) & X is a_partition of Y & ( for d being set holds
( d in X iff d is_min_depend PA,PB ) ) ) by A4; ::_thesis: verum
end;
uniqueness
 for b1, b2 being a_partition of Y st ( for d being set holds
( d in b1 iff d is_min_depend PA,PB ) ) & ( for d being set holds
( d in b2 iff d is_min_depend PA,PB ) ) holds
b1 = b2
proof
let A1, A2 be a_partition of Y; ::_thesis: ( ( for d being set holds
( d in A1 iff d is_min_depend PA,PB ) ) & ( for d being set holds
( d in A2 iff d is_min_depend PA,PB ) ) implies A1 = A2 )
assume that
A26: for x being set holds
( x in A1 iff x is_min_depend PA,PB ) and
A27: for x being set holds
( x in A2 iff x is_min_depend PA,PB ) ; ::_thesis: A1 = A2
now__::_thesis:_for_y_being_set_holds_
(_y_in_A1_iff_y_in_A2_)
let y be set ; ::_thesis: ( y in A1 iff y in A2 )
 ( y in A1 iff y is_min_depend PA,PB ) by A26;
hence  ( y in A1 iff y in A2 ) by A27; ::_thesis: verum
end;
hence  A1 = A2 by TARSKI:1; ::_thesis: verum
end;
commutativity
 for b1, PA, PB being a_partition of Y st ( for d being set holds
( d in b1 iff d is_min_depend PA,PB ) ) holds
for d being set holds
( d in b1 iff d is_min_depend PB,PA )
proof
let IT, PA, PB be a_partition of Y; ::_thesis: ( ( for d being set holds
( d in IT iff d is_min_depend PA,PB ) ) implies for d being set holds
( d in IT iff d is_min_depend PB,PA ) )
A28: now__::_thesis:_for_a_being_set_st_a_is_min_depend_PA,PB_holds_
a_is_min_depend_PB,PA
let a be set ; ::_thesis: ( a is_min_depend PA,PB implies a is_min_depend PB,PA )
assume A29: a is_min_depend PA,PB ; ::_thesis: a is_min_depend PB,PA
then A30: ( a is_a_dependent_set_of PB & a is_a_dependent_set_of PA ) by Def2;
 for d being set st d c= a & d is_a_dependent_set_of PB & d is_a_dependent_set_of PA holds
d = a by A29, Def2;
hence  a is_min_depend PB,PA by A30, Def2; ::_thesis: verum
end;
A31: now__::_thesis:_for_a_being_set_st_a_is_min_depend_PB,PA_holds_
a_is_min_depend_PA,PB
let a be set ; ::_thesis: ( a is_min_depend PB,PA implies a is_min_depend PA,PB )
assume A32: a is_min_depend PB,PA ; ::_thesis: a is_min_depend PA,PB
then A33: ( a is_a_dependent_set_of PA & a is_a_dependent_set_of PB ) by Def2;
 for d being set st d c= a & d is_a_dependent_set_of PA & d is_a_dependent_set_of PB holds
d = a by A32, Def2;
hence  a is_min_depend PA,PB by A33, Def2; ::_thesis: verum
end;
 for a being set st ( for d being set holds
( d in a iff d is_min_depend PA,PB ) ) holds
for d being set holds
( d in a iff d is_min_depend PB,PA )
proof
let a be set ; ::_thesis: ( ( for d being set holds
( d in a iff d is_min_depend PA,PB ) ) implies for d being set holds
( d in a iff d is_min_depend PB,PA ) )
assume A34: for d being set holds
( d in a iff d is_min_depend PA,PB ) ; ::_thesis: for d being set holds
( d in a iff d is_min_depend PB,PA )
let d be set ; ::_thesis: ( d in a iff d is_min_depend PB,PA )
A35: ( d in a iff d is_min_depend PA,PB ) by A34;
hence  ( d in a implies d is_min_depend PB,PA ) by A28; ::_thesis: ( d is_min_depend PB,PA implies d in a )
assume  d is_min_depend PB,PA ; ::_thesis: d in a
hence  d in a by A31, A35; ::_thesis: verum
end;
hence  ( ( for d being set holds
( d in IT iff d is_min_depend PA,PB ) ) implies for d being set holds
( d in IT iff d is_min_depend PB,PA ) ) ; ::_thesis: verum
end;
end;

:: deftheorem Def5 defines '\/' PARTIT1:def_5_:_
 for Y being non empty set
for PA, PB, b4 being a_partition of Y holds
( b4 = PA '\/' PB iff for d being set holds
( d in b4 iff d is_min_depend PA,PB ) );

theorem Th16: :: PARTIT1:16
for Y being non empty set
for PA, PB being a_partition of Y holds PA '<' PA '\/' PB
proof
let Y be non empty set ; ::_thesis: for PA, PB being a_partition of Y holds PA '<' PA '\/' PB
thus  for PA, PB being a_partition of Y holds PA '<' PA '\/' PB ::_thesis: verum
proof
let PA, PB be a_partition of Y; ::_thesis: PA '<' PA '\/' PB
 for a being set st a in PA holds
ex b being set st
( b in PA '\/' PB & a c= b )
proof
let a be set ; ::_thesis: ( a in PA implies ex b being set st
( b in PA '\/' PB & a c= b ) )
assume A1: a in PA ; ::_thesis: ex b being set st
( b in PA '\/' PB & a c= b )
then A2: a <> {} by EQREL_1:def_4;
set x = the Element of a;
A3: the Element of a in Y by A1, A2, TARSKI:def_3;
 union (PA '\/' PB) = Y by EQREL_1:def_4;
then consider b being set  such that
A4: the Element of a in b and
A5: b in PA '\/' PB by A3, TARSKI:def_4;
 b is_min_depend PA,PB by A5, Def5;
then  b is_a_dependent_set_of PA by Def2;
then consider B being set  such that
A6: B c= PA and
 B <> {} and
A7: b = union B by Def1;
 a in B
proof
consider u being set  such that
A8: the Element of a in u and
A9: u in B by A4, A7, TARSKI:def_4;
 a /\ u <> {} by A2, A8, XBOOLE_0:def_4;
then A10: not a misses u by XBOOLE_0:def_7;
 u in PA by A6, A9;
hence  a in B by A1, A9, A10, EQREL_1:def_4; ::_thesis: verum
end;
hence  ex b being set st
( b in PA '\/' PB & a c= b ) by A5, A7, ZFMISC_1:74; ::_thesis: verum
end;
hence  PA '<' PA '\/' PB by SETFAM_1:def_2; ::_thesis: verum
end;
end;

theorem :: PARTIT1:17
for Y being non empty set
for PA being a_partition of Y holds PA '\/' PA = PA
proof
let Y be non empty set ; ::_thesis: for PA being a_partition of Y holds PA '\/' PA = PA
let PA be a_partition of Y; ::_thesis: PA '\/' PA = PA
A1: PA '<' PA '\/' PA by Th16;
 for a being set st a in PA '\/' PA holds
ex b being set st
( b in PA & a c= b )
proof
let a be set ; ::_thesis: ( a in PA '\/' PA implies ex b being set st
( b in PA & a c= b ) )
assume A2: a in PA '\/' PA ; ::_thesis: ex b being set st
( b in PA & a c= b )
then A3: a is_min_depend PA,PA by Def5;
then  a is_a_dependent_set_of PA by Def2;
then consider B being set  such that
A4: B c= PA and
 B <> {} and
A5: a = union B by Def1;
A6: a <> {} by A2, EQREL_1:def_4;
set x = the Element of a;
 the Element of a in a by A6;
then  the Element of a in Y by A2;
then  the Element of a in union PA by EQREL_1:def_4;
then consider b being set  such that
A7: the Element of a in b and
A8: b in PA by TARSKI:def_4;
 b in B
proof
consider u being set  such that
A9: the Element of a in u and
A10: u in B by A5, A6, TARSKI:def_4;
 b /\ u <> {} by A7, A9, XBOOLE_0:def_4;
then A11: not b misses u by XBOOLE_0:def_7;
 u in PA by A4, A10;
hence  b in B by A8, A10, A11, EQREL_1:def_4; ::_thesis: verum
end;
then A12: b c= a by A5, ZFMISC_1:74;
 b is_a_dependent_set_of PA by A8, Th6;
then  a = b by A3, A12, Def2;
hence  ex b being set st
( b in PA & a c= b ) by A8; ::_thesis: verum
end;
then  PA '\/' PA '<' PA by SETFAM_1:def_2;
hence  PA '\/' PA = PA by A1, Th4; ::_thesis: verum
end;

theorem Th18: :: PARTIT1:18
for Y being non empty set
for x, z0, t being set
for PA, PC being a_partition of Y st PA '<' PC & x in PC & z0 in PA & t in x & t in z0 holds
z0 c= x
proof
let Y be non empty set ; ::_thesis: for x, z0, t being set
for PA, PC being a_partition of Y st PA '<' PC & x in PC & z0 in PA & t in x & t in z0 holds
z0 c= x
let x, z0, t be set ; ::_thesis: for PA, PC being a_partition of Y st PA '<' PC & x in PC & z0 in PA & t in x & t in z0 holds
z0 c= x
let PA, PC be a_partition of Y; ::_thesis: ( PA '<' PC & x in PC & z0 in PA & t in x & t in z0 implies z0 c= x )
assume that
A1: PA '<' PC and
A2: x in PC and
A3: z0 in PA and
A4: ( t in x & t in z0 ) ; ::_thesis: z0 c= x
consider b being set  such that
A5: b in PC and
A6: z0 c= b by A1, A3, SETFAM_1:def_2;
 ( x = b or x misses b ) by A2, A5, EQREL_1:def_4;
hence  z0 c= x by A4, A6, XBOOLE_0:3; ::_thesis: verum
end;

theorem :: PARTIT1:19
for Y being non empty set
for x, z0, t being set
for PA, PB being a_partition of Y st x in PA '\/' PB & z0 in PA & t in x & t in z0 holds
z0 c= x by Th16, Th18;

begin

definition
let Y be non empty set ;
let PA be a_partition of Y;
func ERl PA ->  Equivalence_Relation of Y means :Def6: :: PARTIT1:def 6
 for x1, x2 being set holds
( [x1,x2] in it iff ex A being Subset of Y st
( A in PA & x1 in A & x2 in A ) );
existence
 ex b1 being Equivalence_Relation of Y st
for x1, x2 being set holds
( [x1,x2] in b1 iff ex A being Subset of Y st
( A in PA & x1 in A & x2 in A ) )
proof
A1: union PA = Y by EQREL_1:def_4;
 ex RA being Equivalence_Relation of Y st
for x, y being set holds
( [x,y] in RA iff ex A being Subset of Y st
( A in PA & x in A & y in A ) )
proof
defpred S1[ set , set ] means  ex A being Subset of Y st
( A in PA & $1 in A & $2 in A );
A2: for x being set st x in Y holds
S1[x,x]
proof
let x be set ; ::_thesis: ( x in Y implies S1[x,x] )
assume  x in Y ; ::_thesis: S1[x,x]
then  ex Z being set st
( x in Z & Z in PA ) by A1, TARSKI:def_4;
then consider Z being non empty set  such that
A3: x in Z and
A4: Z in PA ;
reconsider A = Z as Subset of Y by A4;
take  A ; ::_thesis: ( A in PA & x in A & x in A )
thus  ( A in PA & x in A & x in A ) by A3, A4; ::_thesis: verum
end;
A5: for x, y being set st S1[x,y] holds
S1[y,x] ;
A6: for x, y, z being set st S1[x,y] & S1[y,z] holds
S1[x,z]
proof
let x, y, z be set ; ::_thesis: ( S1[x,y] & S1[y,z] implies S1[x,z] )
given A being Subset of Y such that A7: A in PA and
A8: ( x in A & y in A ) ; ::_thesis: ( not S1[y,z] or S1[x,z] )
given B being Subset of Y such that A9: B in PA and
A10: ( y in B & z in B ) ; ::_thesis: S1[x,z]
 ( A = B or A misses B ) by A7, A9, EQREL_1:def_4;
hence  S1[x,z] by A7, A8, A10, XBOOLE_0:3; ::_thesis: verum
end;
consider RA being Equivalence_Relation of Y such that
A11: for x, y being set holds
( [x,y] in RA iff ( x in Y & y in Y & S1[x,y] ) ) from EQREL_1:sch_1(A2, A5, A6);
take  RA ; ::_thesis: for x, y being set holds
( [x,y] in RA iff ex A being Subset of Y st
( A in PA & x in A & y in A ) )
thus  for x, y being set holds
( [x,y] in RA iff ex A being Subset of Y st
( A in PA & x in A & y in A ) ) by A11; ::_thesis: verum
end;
hence  ex b1 being Equivalence_Relation of Y st
for x1, x2 being set holds
( [x1,x2] in b1 iff ex A being Subset of Y st
( A in PA & x1 in A & x2 in A ) ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Equivalence_Relation of Y st ( for x1, x2 being set holds
( [x1,x2] in b1 iff ex A being Subset of Y st
( A in PA & x1 in A & x2 in A ) ) ) & ( for x1, x2 being set holds
( [x1,x2] in b2 iff ex A being Subset of Y st
( A in PA & x1 in A & x2 in A ) ) ) holds
b1 = b2
proof
let f1, f2 be Equivalence_Relation of Y; ::_thesis: ( ( for x1, x2 being set holds
( [x1,x2] in f1 iff ex A being Subset of Y st
( A in PA & x1 in A & x2 in A ) ) ) & ( for x1, x2 being set holds
( [x1,x2] in f2 iff ex A being Subset of Y st
( A in PA & x1 in A & x2 in A ) ) ) implies f1 = f2 )
assume that
A12: for x1, x2 being set holds
( [x1,x2] in f1 iff ex A being Subset of Y st
( A in PA & x1 in A & x2 in A ) ) and
A13: for x1, x2 being set holds
( [x1,x2] in f2 iff ex A being Subset of Y st
( A in PA & x1 in A & x2 in A ) ) ; ::_thesis: f1 = f2
let x1, x2 be set ; :: according to RELAT_1:def_2 ::_thesis: ( ( not [x1,x2] in f1 or [x1,x2] in f2 ) & ( not [x1,x2] in f2 or [x1,x2] in f1 ) )
 ( [x1,x2] in f1 iff ex A being Subset of Y st
( A in PA & x1 in A & x2 in A ) ) by A12;
hence  ( ( not [x1,x2] in f1 or [x1,x2] in f2 ) & ( not [x1,x2] in f2 or [x1,x2] in f1 ) ) by A13; ::_thesis: verum
end;
end;

:: deftheorem Def6 defines ERl PARTIT1:def_6_:_
 for Y being non empty set
for PA being a_partition of Y
for b3 being Equivalence_Relation of Y holds
( b3 = ERl PA iff for x1, x2 being set holds
( [x1,x2] in b3 iff ex A being Subset of Y st
( A in PA & x1 in A & x2 in A ) ) );

definition
let Y be non empty set ;
defpred S1[ set , set ] means  ex PA being a_partition of Y st
( PA = $1 & $2 = ERl PA );
A1: for x being set st x in PARTITIONS Y holds
ex z being set st S1[x,z]
proof
let x be set ; ::_thesis: ( x in PARTITIONS Y implies ex z being set st S1[x,z] )
assume  x in PARTITIONS Y ; ::_thesis: ex z being set st S1[x,z]
then reconsider x = x as a_partition of Y by Def3;
take  ERl x ; ::_thesis: S1[x, ERl x]
thus  S1[x, ERl x] ; ::_thesis: verum
end;
func Rel Y ->  Function means :: PARTIT1:def 7
( dom it = PARTITIONS Y & ( for x being set st x in PARTITIONS Y holds
ex PA being a_partition of Y st
( PA = x & it . x = ERl PA ) ) );
existence
 ex b1 being Function st
( dom b1 = PARTITIONS Y & ( for x being set st x in PARTITIONS Y holds
ex PA being a_partition of Y st
( PA = x & b1 . x = ERl PA ) ) )
proof
thus  ex f being Function st
( dom f = PARTITIONS Y & ( for x being set st x in PARTITIONS Y holds
S1[x,f . x] ) ) from CLASSES1:sch_1(A1); ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function st dom b1 = PARTITIONS Y & ( for x being set st x in PARTITIONS Y holds
ex PA being a_partition of Y st
( PA = x & b1 . x = ERl PA ) ) & dom b2 = PARTITIONS Y & ( for x being set st x in PARTITIONS Y holds
ex PA being a_partition of Y st
( PA = x & b2 . x = ERl PA ) ) holds
b1 = b2
proof
let f1, f2 be Function; ::_thesis: ( dom f1 = PARTITIONS Y & ( for x being set st x in PARTITIONS Y holds
ex PA being a_partition of Y st
( PA = x & f1 . x = ERl PA ) ) & dom f2 = PARTITIONS Y & ( for x being set st x in PARTITIONS Y holds
ex PA being a_partition of Y st
( PA = x & f2 . x = ERl PA ) ) implies f1 = f2 )
assume that
A2: dom f1 = PARTITIONS Y and
A3: for x being set st x in PARTITIONS Y holds
ex PA being a_partition of Y st
( PA = x & f1 . x = ERl PA ) and
A4: dom f2 = PARTITIONS Y and
A5: for x being set st x in PARTITIONS Y holds
ex PA being a_partition of Y st
( PA = x & f2 . x = ERl PA ) ; ::_thesis: f1 = f2
 for z being set st z in PARTITIONS Y holds
f1 . z = f2 . z
proof
let x be set ; ::_thesis: ( x in PARTITIONS Y implies f1 . x = f2 . x )
assume  x in PARTITIONS Y ; ::_thesis: f1 . x = f2 . x
then  ( ex PA being a_partition of Y st
( PA = x & f1 . x = ERl PA ) & ex PA being a_partition of Y st
( PA = x & f2 . x = ERl PA ) ) by A3, A5;
hence  f1 . x = f2 . x ; ::_thesis: verum
end;
hence  f1 = f2 by A2, A4, FUNCT_1:2; ::_thesis: verum
end;
end;

:: deftheorem  defines Rel PARTIT1:def_7_:_
 for Y being non empty set
for b2 being Function holds
( b2 = Rel Y iff ( dom b2 = PARTITIONS Y & ( for x being set st x in PARTITIONS Y holds
ex PA being a_partition of Y st
( PA = x & b2 . x = ERl PA ) ) ) );

theorem Th20: :: PARTIT1:20
for Y being non empty set
for PA, PB being a_partition of Y holds
( PA '<' PB iff ERl PA c= ERl PB )
proof
let Y be non empty set ; ::_thesis: for PA, PB being a_partition of Y holds
( PA '<' PB iff ERl PA c= ERl PB )
let PA, PB be a_partition of Y; ::_thesis: ( PA '<' PB iff ERl PA c= ERl PB )
set RA = ERl PA;
set RB = ERl PB;
hereby  ::_thesis: ( ERl PA c= ERl PB implies PA '<' PB )
assume A1: PA '<' PB ; ::_thesis: ERl PA c= ERl PB
 for x1, x2 being set st [x1,x2] in ERl PA holds
[x1,x2] in ERl PB
proof
let x1, x2 be set ; ::_thesis: ( [x1,x2] in ERl PA implies [x1,x2] in ERl PB )
assume  [x1,x2] in ERl PA ; ::_thesis: [x1,x2] in ERl PB
then consider A being Subset of Y such that
A2: A in PA and
A3: ( x1 in A & x2 in A ) by Def6;
 ex y being set st
( y in PB & A c= y ) by A1, A2, SETFAM_1:def_2;
hence  [x1,x2] in ERl PB by A3, Def6; ::_thesis: verum
end;
hence  ERl PA c= ERl PB by RELAT_1:def_3; ::_thesis: verum
end;
assume A4: ERl PA c= ERl PB ; ::_thesis: PA '<' PB
 for x being set st x in PA holds
ex y being set st
( y in PB & x c= y )
proof
let x be set ; ::_thesis: ( x in PA implies ex y being set st
( y in PB & x c= y ) )
assume A5: x in PA ; ::_thesis: ex y being set st
( y in PB & x c= y )
then A6: x <> {} by EQREL_1:def_4;
set x0 = the Element of x;
set y =  {  z where z is Element of Y : [ the Element of x,z] in ERl PB  }  ;
A7: x c=  {  z where z is Element of Y : [ the Element of x,z] in ERl PB  }
proof
let x1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not x1 in x or x1 in  {  z where z is Element of Y : [ the Element of x,z] in ERl PB  }  )
assume A8: x1 in x ; ::_thesis: x1 in  {  z where z is Element of Y : [ the Element of x,z] in ERl PB  }
then  [ the Element of x,x1] in ERl PA by A5, Def6;
hence  x1 in  {  z where z is Element of Y : [ the Element of x,z] in ERl PB  }  by A4, A5, A8; ::_thesis: verum
end;
set x1 = the Element of x;
 [ the Element of x, the Element of x] in ERl PA by A5, A6, Def6;
then consider B being Subset of Y such that
A9: B in PB and
A10: the Element of x in B and
 the Element of x in B by A4, Def6;
A11:  {  z where z is Element of Y : [ the Element of x,z] in ERl PB  }  c= B
proof
let x2 be set ; :: according to TARSKI:def_3 ::_thesis: ( not x2 in  {  z where z is Element of Y : [ the Element of x,z] in ERl PB  }  or x2 in B )
assume  x2 in  {  z where z is Element of Y : [ the Element of x,z] in ERl PB  }  ; ::_thesis: x2 in B
then  ex z being Element of Y st
( z = x2 & [ the Element of x,z] in ERl PB ) ;
then consider B2 being Subset of Y such that
A12: B2 in PB and
A13: the Element of x in B2 and
A14: x2 in B2 by Def6;
 B2 meets B by A10, A13, XBOOLE_0:3;
hence  x2 in B by A9, A12, A14, EQREL_1:def_4; ::_thesis: verum
end;
 B c=  {  z where z is Element of Y : [ the Element of x,z] in ERl PB  }
proof
let x2 be set ; :: according to TARSKI:def_3 ::_thesis: ( not x2 in B or x2 in  {  z where z is Element of Y : [ the Element of x,z] in ERl PB  }  )
assume A15: x2 in B ; ::_thesis: x2 in  {  z where z is Element of Y : [ the Element of x,z] in ERl PB  }
then  [ the Element of x,x2] in ERl PB by A9, A10, Def6;
hence  x2 in  {  z where z is Element of Y : [ the Element of x,z] in ERl PB  }  by A15; ::_thesis: verum
end;
then   {  z where z is Element of Y : [ the Element of x,z] in ERl PB  }  = B by A11, XBOOLE_0:def_10;
hence  ex y being set st
( y in PB & x c= y ) by A7, A9; ::_thesis: verum
end;
hence  PA '<' PB by SETFAM_1:def_2; ::_thesis: verum
end;

theorem Th21: :: PARTIT1:21
for Y being non empty set
for PA, PB being a_partition of Y
for p0, x, y being set
for f being FinSequence of Y st p0 c= Y & x in p0 & f . 1 = x & f . (len f) = y & 1 <= len f & ( for i being Element of NAT st 1 <= i & i < len f holds
ex p2, p3, u being set st
( p2 in PA & p3 in PB & f . i in p2 & u in p2 & u in p3 & f . (i + 1) in p3 ) ) & p0 is_a_dependent_set_of PA & p0 is_a_dependent_set_of PB holds
y in p0
proof
let Y be non empty set ; ::_thesis: for PA, PB being a_partition of Y
for p0, x, y being set
for f being FinSequence of Y st p0 c= Y & x in p0 & f . 1 = x & f . (len f) = y & 1 <= len f & ( for i being Element of NAT st 1 <= i & i < len f holds
ex p2, p3, u being set st
( p2 in PA & p3 in PB & f . i in p2 & u in p2 & u in p3 & f . (i + 1) in p3 ) ) & p0 is_a_dependent_set_of PA & p0 is_a_dependent_set_of PB holds
y in p0
let PA, PB be a_partition of Y; ::_thesis: for p0, x, y being set
for f being FinSequence of Y st p0 c= Y & x in p0 & f . 1 = x & f . (len f) = y & 1 <= len f & ( for i being Element of NAT st 1 <= i & i < len f holds
ex p2, p3, u being set st
( p2 in PA & p3 in PB & f . i in p2 & u in p2 & u in p3 & f . (i + 1) in p3 ) ) & p0 is_a_dependent_set_of PA & p0 is_a_dependent_set_of PB holds
y in p0
let p0, x, y be set ; ::_thesis: for f being FinSequence of Y st p0 c= Y & x in p0 & f . 1 = x & f . (len f) = y & 1 <= len f & ( for i being Element of NAT st 1 <= i & i < len f holds
ex p2, p3, u being set st
( p2 in PA & p3 in PB & f . i in p2 & u in p2 & u in p3 & f . (i + 1) in p3 ) ) & p0 is_a_dependent_set_of PA & p0 is_a_dependent_set_of PB holds
y in p0
let f be FinSequence of Y; ::_thesis: ( p0 c= Y & x in p0 & f . 1 = x & f . (len f) = y & 1 <= len f & ( for i being Element of NAT st 1 <= i & i < len f holds
ex p2, p3, u being set st
( p2 in PA & p3 in PB & f . i in p2 & u in p2 & u in p3 & f . (i + 1) in p3 ) ) & p0 is_a_dependent_set_of PA & p0 is_a_dependent_set_of PB implies y in p0 )
assume that
A1: p0 c= Y and
A2: ( x in p0 & f . 1 = x ) and
A3: ( f . (len f) = y & 1 <= len f ) and
A4: for i being Element of NAT st 1 <= i & i < len f holds
ex p2, p3, u being set st
( p2 in PA & p3 in PB & f . i in p2 & u in p2 & u in p3 & f . (i + 1) in p3 ) and
A5: p0 is_a_dependent_set_of PA and
A6: p0 is_a_dependent_set_of PB ; ::_thesis: y in p0
consider A1 being set  such that
A7: A1 c= PA and
 A1 <> {} and
A8: p0 = union A1 by A5, Def1;
consider B1 being set  such that
A9: B1 c= PB and
 B1 <> {} and
A10: p0 = union B1 by A6, Def1;
A11: union PA = Y by EQREL_1:def_4;
A12: for A being set st A in PA holds
( A <> {} & ( for B being set holds
( not B in PA or A = B or A misses B ) ) ) by EQREL_1:def_4;
A13: for A being set st A in PB holds
( A <> {} & ( for B being set holds
( not B in PB or A = B or A misses B ) ) ) by EQREL_1:def_4;
 for k being Element of NAT st 1 <= k & k <= len f holds
f . k in p0
proof
defpred S1[ Element of NAT ] means ( 1 <= $1 & $1 <= len f implies f . $1 in p0 );
A14: S1[ 0 ] ;
A15: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A16: S1[k] ; ::_thesis: S1[k + 1]
assume that
A17: 1 <= k + 1 and
A18: k + 1 <= len f ; ::_thesis: f . (k + 1) in p0
A19: k < len f by A18, NAT_1:13;
A20: ( 1 <= k or 1 = k + 1 ) by A17, NAT_1:8;
now__::_thesis:_f_._(k_+_1)_in_p0
percases ( 1 <= k or 0 = k ) by A20;
supposeA21: 1 <= k ; ::_thesis: f . (k + 1) in p0
then consider p2, p3, u being set  such that
A22: p2 in PA and
A23: p3 in PB and
A24: f . k in p2 and
A25: u in p2 and
A26: u in p3 and
A27: f . (k + 1) in p3 by A4, A19;
consider A being set  such that
A28: f . k in A and
A29: A in PA by A1, A11, A16, A18, A21, NAT_1:13, TARSKI:def_4;
A30: ( p2 = A or p2 misses A ) by A22, A29, EQREL_1:def_4;
consider a being set  such that
A31: f . k in a and
A32: a in A1 by A8, A16, A18, A21, NAT_1:13, TARSKI:def_4;
 ( a = p2 or a misses p2 ) by A7, A12, A22, A32;
then A33: A c= p0 by A8, A24, A28, A30, A31, A32, XBOOLE_0:3, ZFMISC_1:74;
consider B being set  such that
A34: u in B and
A35: B in PB by A23, A26;
A36: ( p3 = B or p3 misses B ) by A23, A35, EQREL_1:def_4;
consider b being set  such that
A37: u in b and
A38: b in B1 by A10, A24, A25, A28, A30, A33, TARSKI:def_4, XBOOLE_0:3;
 ( p3 = b or p3 misses b ) by A9, A13, A23, A38;
then  B c= p0 by A10, A26, A34, A36, A37, A38, XBOOLE_0:3, ZFMISC_1:74;
hence  f . (k + 1) in p0 by A26, A27, A34, A36, XBOOLE_0:3; ::_thesis: verum
end;
suppose 0 = k ; ::_thesis: f . (k + 1) in p0
hence  f . (k + 1) in p0 by A2; ::_thesis: verum
end;
end;
end;
hence  f . (k + 1) in p0 ; ::_thesis: verum
end;
thus  for k being Element of NAT holds S1[k] from NAT_1:sch_1(A14, A15); ::_thesis: verum
end;
hence  y in p0 by A3; ::_thesis: verum
end;

theorem Th22: :: PARTIT1:22
for Y being non empty set
for R1, R2 being Equivalence_Relation of Y
for f being FinSequence of Y
for x, y being set st x in Y & f . 1 = x & f . (len f) = y & 1 <= len f & ( for i being Element of NAT st 1 <= i & i < len f holds
ex u being set st
( u in Y & [(f . i),u] in R1 \/ R2 & [u,(f . (i + 1))] in R1 \/ R2 ) ) holds
[x,y] in R1 "\/" R2
proof
let Y be non empty set ; ::_thesis: for R1, R2 being Equivalence_Relation of Y
for f being FinSequence of Y
for x, y being set st x in Y & f . 1 = x & f . (len f) = y & 1 <= len f & ( for i being Element of NAT st 1 <= i & i < len f holds
ex u being set st
( u in Y & [(f . i),u] in R1 \/ R2 & [u,(f . (i + 1))] in R1 \/ R2 ) ) holds
[x,y] in R1 "\/" R2
let R1, R2 be Equivalence_Relation of Y; ::_thesis: for f being FinSequence of Y
for x, y being set st x in Y & f . 1 = x & f . (len f) = y & 1 <= len f & ( for i being Element of NAT st 1 <= i & i < len f holds
ex u being set st
( u in Y & [(f . i),u] in R1 \/ R2 & [u,(f . (i + 1))] in R1 \/ R2 ) ) holds
[x,y] in R1 "\/" R2
let f be FinSequence of Y; ::_thesis: for x, y being set st x in Y & f . 1 = x & f . (len f) = y & 1 <= len f & ( for i being Element of NAT st 1 <= i & i < len f holds
ex u being set st
( u in Y & [(f . i),u] in R1 \/ R2 & [u,(f . (i + 1))] in R1 \/ R2 ) ) holds
[x,y] in R1 "\/" R2
let x, y be set ; ::_thesis: ( x in Y & f . 1 = x & f . (len f) = y & 1 <= len f & ( for i being Element of NAT st 1 <= i & i < len f holds
ex u being set st
( u in Y & [(f . i),u] in R1 \/ R2 & [u,(f . (i + 1))] in R1 \/ R2 ) ) implies [x,y] in R1 "\/" R2 )
assume that
A1: x in Y and
A2: f . 1 = x and
A3: ( f . (len f) = y & 1 <= len f ) and
A4: for i being Element of NAT st 1 <= i & i < len f holds
ex u being set st
( u in Y & [(f . i),u] in R1 \/ R2 & [u,(f . (i + 1))] in R1 \/ R2 ) ; ::_thesis: [x,y] in R1 "\/" R2
 for i being Element of NAT st 1 <= i & i <= len f holds
[(f . 1),(f . i)] in R1 "\/" R2
proof
defpred S1[ Element of NAT ] means ( 1 <= $1 & $1 <= len f implies [(f . 1),(f . $1)] in R1 "\/" R2 );
A5: S1[ 0 ] ;
A6: for i being Element of NAT st S1[i] holds
S1[i + 1]
proof
let i be Element of NAT ; ::_thesis: ( S1[i] implies S1[i + 1] )
assume A7: S1[i] ; ::_thesis: S1[i + 1]
assume that
A8: 1 <= i + 1 and
A9: i + 1 <= len f ; ::_thesis: [(f . 1),(f . (i + 1))] in R1 "\/" R2
A10: i < len f by A9, NAT_1:13;
A11: ( 1 <= i or 1 = i + 1 ) by A8, NAT_1:8;
A12: R1 \/ R2 c= R1 "\/" R2 by EQREL_1:def_2;
now__::_thesis:_[(f_._1),(f_._(i_+_1))]_in_R1_"\/"_R2
percases ( 1 <= i or 0 = i ) by A11;
supposeA13: 1 <= i ; ::_thesis: [(f . 1),(f . (i + 1))] in R1 "\/" R2
then consider u being set  such that
A14: u in Y and
A15: ( [(f . i),u] in R1 \/ R2 & [u,(f . (i + 1))] in R1 \/ R2 ) by A4, A10;
reconsider u = u as Element of Y by A14;
A16: dom f = Seg (len f) by FINSEQ_1:def_3;
then  i in dom f by A10, A13, FINSEQ_1:1;
then reconsider f1 = f . i as Element of Y by FINSEQ_2:11;
 i + 1 in dom f by A8, A9, A16, FINSEQ_1:1;
then reconsider f2 = f . (i + 1) as Element of Y by FINSEQ_2:11;
reconsider p = <*f1,u,f2*> as FinSequence of Y ;
A17: len p = 3 by FINSEQ_1:45;
A18: ( p . 1 = f . i & p . 3 = f . (i + 1) ) by FINSEQ_1:45;
 for j being Element of NAT st 1 <= j & j < len p holds
[(p . j),(p . (j + 1))] in R1 \/ R2
proof
let j be Element of NAT ; ::_thesis: ( 1 <= j & j < len p implies [(p . j),(p . (j + 1))] in R1 \/ R2 )
assume that
A19: 1 <= j and
A20: j < len p ; ::_thesis: [(p . j),(p . (j + 1))] in R1 \/ R2
 j < 2 + 1 by A20, FINSEQ_1:45;
then  j <= 2 by NAT_1:13;
then  ( j = 0 or j = 1 or j = 2 ) by NAT_1:26;
hence  [(p . j),(p . (j + 1))] in R1 \/ R2 by A15, A18, A19, FINSEQ_1:45; ::_thesis: verum
end;
then  [(f . i),(f . (i + 1))] in R1 "\/" R2 by A17, A18, EQREL_1:28;
hence  [(f . 1),(f . (i + 1))] in R1 "\/" R2 by A7, A9, A13, EQREL_1:7, NAT_1:13; ::_thesis: verum
end;
supposeA21: 0 = i ; ::_thesis: [(f . 1),(f . (i + 1))] in R1 "\/" R2
 [(f . 1),(f . 1)] in R1 by A1, A2, EQREL_1:5;
then  [(f . 1),(f . 1)] in R1 \/ R2 by XBOOLE_0:def_3;
hence  [(f . 1),(f . (i + 1))] in R1 "\/" R2 by A12, A21; ::_thesis: verum
end;
end;
end;
hence  [(f . 1),(f . (i + 1))] in R1 "\/" R2 ; ::_thesis: verum
end;
thus  for i being Element of NAT holds S1[i] from NAT_1:sch_1(A5, A6); ::_thesis: verum
end;
hence  [x,y] in R1 "\/" R2 by A2, A3; ::_thesis: verum
end;

theorem Th23: :: PARTIT1:23
for Y being non empty set
for PA, PB being a_partition of Y holds ERl (PA '\/' PB) = (ERl PA) "\/" (ERl PB)
proof
let Y be non empty set ; ::_thesis: for PA, PB being a_partition of Y holds ERl (PA '\/' PB) = (ERl PA) "\/" (ERl PB)
let PA, PB be a_partition of Y; ::_thesis: ERl (PA '\/' PB) = (ERl PA) "\/" (ERl PB)
A1: PA is_finer_than PA '\/' PB by Th16;
A2: PB is_finer_than PA '\/' PB by Th16;
A3: union PA = Y by EQREL_1:def_4;
A4: union PB = Y by EQREL_1:def_4;
A5: ERl (PA '\/' PB) c= (ERl PA) "\/" (ERl PB)
proof
let x, y be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [x,y] in ERl (PA '\/' PB) or [x,y] in (ERl PA) "\/" (ERl PB) )
assume  [x,y] in ERl (PA '\/' PB) ; ::_thesis: [x,y] in (ERl PA) "\/" (ERl PB)
then consider p0 being Subset of Y such that
A6: p0 in PA '\/' PB and
A7: x in p0 and
A8: y in p0 by Def6;
A9: p0 is_min_depend PA,PB by A6, Def5;
then A10: p0 is_a_dependent_set_of PA by Def2;
A11: p0 is_a_dependent_set_of PB by A9, Def2;
consider A1 being set  such that
A12: A1 c= PA and
 A1 <> {} and
A13: p0 = union A1 by A10, Def1;
consider a being set  such that
A14: x in a and
A15: a in A1 by A7, A13, TARSKI:def_4;
reconsider Ca =  {  p where p is Element of PA : ex f being FinSequence of Y st
( 1 <= len f & f . 1 = x & f . (len f) in p & ( for i being Element of NAT st 1 <= i & i < len f holds
ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 ) ) )  }  as set ;
reconsider pb = union Ca as set ;
reconsider Cb =  {  p where p is Element of PB : ex q being set st
( q in Ca & p /\ q <> {} )  }  as set ;
reconsider x9 = x as Element of Y by A7;
reconsider fx = <*x9*> as FinSequence of Y ;
A16: fx . 1 = x by FINSEQ_1:def_8;
then A17: fx . (len fx) in a by A14, FINSEQ_1:40;
 ( 1 <= len fx & ( for i being Element of NAT st 1 <= i & i < len fx holds
ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & fx . i in p1 & x0 in p1 /\ p2 & fx . (i + 1) in p2 ) ) ) by FINSEQ_1:40;
then A18: a in Ca by A12, A15, A16, A17;
then consider y5 being set  such that
A19: x in y5 and
A20: y5 in Ca by A14;
consider z5 being set  such that
A21: x9 in z5 and
A22: z5 in PB by A4, TARSKI:def_4;
 y5 /\ z5 <> {} by A19, A21, XBOOLE_0:def_4;
then A23: z5 in Cb by A20, A22;
 Ca c= PA
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in Ca or z in PA )
assume  z in Ca ; ::_thesis: z in PA
then  ex p being Element of PA st
( z = p & ex f being FinSequence of Y st
( 1 <= len f & f . 1 = x & f . (len f) in p & ( for i being Element of NAT st 1 <= i & i < len f holds
ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 ) ) ) ) ;
hence  z in PA ; ::_thesis: verum
end;
then A24: pb is_a_dependent_set_of PA by A18, Def1;
A25: pb c= union Cb
proof
let x1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not x1 in pb or x1 in union Cb )
assume  x1 in pb ; ::_thesis: x1 in union Cb
then consider y being set  such that
A26: x1 in y and
A27: y in Ca by TARSKI:def_4;
 ex p being Element of PA st
( y = p & ex f being FinSequence of Y st
( 1 <= len f & f . 1 = x & f . (len f) in p & ( for i being Element of NAT st 1 <= i & i < len f holds
ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 ) ) ) ) by A27;
then consider z being set  such that
A28: x1 in z and
A29: z in PB by A4, A26, TARSKI:def_4;
 y /\ z <> {} by A26, A28, XBOOLE_0:def_4;
then  z in Cb by A27, A29;
hence  x1 in union Cb by A28, TARSKI:def_4; ::_thesis: verum
end;
 union Cb c= pb
proof
let x1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not x1 in union Cb or x1 in pb )
assume  x1 in union Cb ; ::_thesis: x1 in pb
then consider y1 being set  such that
A30: x1 in y1 and
A31: y1 in Cb by TARSKI:def_4;
A32: ex p being Element of PB st
( y1 = p & ex q being set st
( q in Ca & p /\ q <> {} ) ) by A31;
then consider q being set  such that
A33: q in Ca and
A34: y1 /\ q <> {} ;
consider pd being set  such that
A35: x1 in pd and
A36: pd in PA by A3, A30, A32, TARSKI:def_4;
A37: ex pp being Element of PA st
( q = pp & ex f being FinSequence of Y st
( 1 <= len f & f . 1 = x & f . (len f) in pp & ( for i being Element of NAT st 1 <= i & i < len f holds
ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 ) ) ) ) by A33;
then consider fd being FinSequence of Y such that
A38: 1 <= len fd and
A39: fd . 1 = x and
A40: fd . (len fd) in q and
A41: for i being Element of NAT st 1 <= i & i < len fd holds
ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & fd . i in p1 & x0 in p1 /\ p2 & fd . (i + 1) in p2 ) ;
reconsider x1 = x1 as Element of Y by A30, A32;
reconsider f = fd ^ <*x1*> as FinSequence of Y ;
 len f = (len fd) + (len <*x1*>) by FINSEQ_1:22;
then A42: len f = (len fd) + 1 by FINSEQ_1:40;
 1 + 1 <= (len fd) + 1 by A38, XREAL_1:6;
then A43: 1 <= len f by A42, XXREAL_0:2;
A44: f . ((len fd) + 1) in y1 by A30, FINSEQ_1:42;
 y1 meets q by A34, XBOOLE_0:def_7;
then consider z0 being set  such that
A45: ( z0 in y1 & z0 in q ) by XBOOLE_0:3;
A46: z0 in y1 /\ q by A45, XBOOLE_0:def_4;
A47: dom fd = Seg (len fd) by FINSEQ_1:def_3;
A48: for k being Element of NAT st 1 <= k & k <= len fd holds
f . k = fd . k
proof
let k be Element of NAT ; ::_thesis: ( 1 <= k & k <= len fd implies f . k = fd . k )
assume  ( 1 <= k & k <= len fd ) ; ::_thesis: f . k = fd . k
then  k in dom fd by A47, FINSEQ_1:1;
hence  f . k = fd . k by FINSEQ_1:def_7; ::_thesis: verum
end;
then A49: ( (fd ^ <*x1*>) . ((len fd) + 1) = x1 & f . 1 = x ) by A38, A39, FINSEQ_1:42;
A50: f . (len fd) in q by A38, A40, A48;
A51: for i being Element of NAT st 1 <= i & i < len fd holds
ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 )
proof
let i be Element of NAT ; ::_thesis: ( 1 <= i & i < len fd implies ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 ) )
assume A52: ( 1 <= i & i < len fd ) ; ::_thesis: ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 )
then A53: f . i = fd . i by A48;
 ( 1 <= i + 1 & i + 1 <= len fd ) by A52, NAT_1:13;
then  f . (i + 1) = fd . (i + 1) by A48;
hence  ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 ) by A41, A52, A53; ::_thesis: verum
end;
 for i being Element of NAT st 1 <= i & i < len f holds
ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 )
proof
let i be Element of NAT ; ::_thesis: ( 1 <= i & i < len f implies ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 ) )
assume that
A54: 1 <= i and
A55: i < len f ; ::_thesis: ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 )
A56: i <= len fd by A42, A55, NAT_1:13;
now__::_thesis:_(_(_1_<=_i_&_i_<_len_fd_&_ex_p1,_p2,_x0_being_set_st_
(_p1_in_PA_&_p2_in_PB_&_f_._i_in_p1_&_x0_in_p1_/\_p2_&_f_._(i_+_1)_in_p2_)_)_or_(_1_<=_i_&_i_=_len_fd_&_ex_p1,_p2,_x0_being_set_st_
(_p1_in_PA_&_p2_in_PB_&_f_._i_in_p1_&_x0_in_p1_/\_p2_&_f_._(i_+_1)_in_p2_)_)_)
percases ( ( 1 <= i & i < len fd ) or ( 1 <= i & i = len fd ) ) by A54, A56, XXREAL_0:1;
case ( 1 <= i & i < len fd ) ; ::_thesis: ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 )
hence  ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 ) by A51; ::_thesis: verum
end;
case ( 1 <= i & i = len fd ) ; ::_thesis: ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 )
hence  ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 ) by A32, A37, A44, A46, A50; ::_thesis: verum
end;
end;
end;
hence  ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 ) ; ::_thesis: verum
end;
then  pd in Ca by A35, A36, A42, A43, A49;
hence  x1 in pb by A35, TARSKI:def_4; ::_thesis: verum
end;
then A57: pb = union Cb by A25, XBOOLE_0:def_10;
 Cb c= PB
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in Cb or z in PB )
assume  z in Cb ; ::_thesis: z in PB
then  ex p being Element of PB st
( z = p & ex q being set st
( q in Ca & p /\ q <> {} ) ) ;
hence  z in PB ; ::_thesis: verum
end;
then A58: pb is_a_dependent_set_of PB by A23, A57, Def1;
now__::_thesis:_pb_c=_p0
assume  not pb c= p0 ; ::_thesis: contradiction
then  pb \ p0 <> {} by XBOOLE_1:37;
then consider x1 being set  such that
A59: x1 in pb \ p0 by XBOOLE_0:def_1;
A60: not x1 in p0 by A59, XBOOLE_0:def_5;
consider y1 being set  such that
A61: x1 in y1 and
A62: y1 in Cb by A57, A59, TARSKI:def_4;
A63: ex p being Element of PB st
( y1 = p & ex q being set st
( q in Ca & p /\ q <> {} ) ) by A62;
then consider q being set  such that
A64: q in Ca and
A65: y1 /\ q <> {} ;
A66: ex pp being Element of PA st
( q = pp & ex f being FinSequence of Y st
( 1 <= len f & f . 1 = x & f . (len f) in pp & ( for i being Element of NAT st 1 <= i & i < len f holds
ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 ) ) ) ) by A64;
then consider fd being FinSequence of Y such that
A67: 1 <= len fd and
A68: fd . 1 = x and
A69: fd . (len fd) in q and
A70: for i being Element of NAT st 1 <= i & i < len fd holds
ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & fd . i in p1 & x0 in p1 /\ p2 & fd . (i + 1) in p2 ) ;
reconsider x1 = x1 as Element of Y by A61, A63;
reconsider f = fd ^ <*x1*> as FinSequence of Y ;
 len f = (len fd) + (len <*x1*>) by FINSEQ_1:22;
then A71: len f = (len fd) + 1 by FINSEQ_1:40;
 1 + 1 <= (len fd) + 1 by A67, XREAL_1:6;
then A72: 1 <= len f by A71, XXREAL_0:2;
A73: f . ((len fd) + 1) in y1 by A61, FINSEQ_1:42;
 y1 meets q by A65, XBOOLE_0:def_7;
then consider z0 being set  such that
A74: ( z0 in y1 & z0 in q ) by XBOOLE_0:3;
A75: z0 in y1 /\ q by A74, XBOOLE_0:def_4;
A76: dom fd = Seg (len fd) by FINSEQ_1:def_3;
A77: for k being Element of NAT st 1 <= k & k <= len fd holds
f . k = fd . k
proof
let k be Element of NAT ; ::_thesis: ( 1 <= k & k <= len fd implies f . k = fd . k )
assume  ( 1 <= k & k <= len fd ) ; ::_thesis: f . k = fd . k
then  k in dom fd by A76, FINSEQ_1:1;
hence  f . k = fd . k by FINSEQ_1:def_7; ::_thesis: verum
end;
then A78: ( (fd ^ <*x1*>) . ((len fd) + 1) = x1 & f . 1 = x ) by A67, A68, FINSEQ_1:42;
A79: f . (len fd) in q by A67, A69, A77;
A80: for i being Element of NAT st 1 <= i & i < len fd holds
ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 )
proof
let i be Element of NAT ; ::_thesis: ( 1 <= i & i < len fd implies ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 ) )
assume A81: ( 1 <= i & i < len fd ) ; ::_thesis: ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 )
then A82: f . i = fd . i by A77;
 ( 1 <= i + 1 & i + 1 <= len fd ) by A81, NAT_1:13;
then  f . (i + 1) = fd . (i + 1) by A77;
hence  ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 ) by A70, A81, A82; ::_thesis: verum
end;
A83: for i being Element of NAT st 1 <= i & i < len f holds
ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 )
proof
let i be Element of NAT ; ::_thesis: ( 1 <= i & i < len f implies ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 ) )
assume that
A84: 1 <= i and
A85: i < len f ; ::_thesis: ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 )
A86: i <= len fd by A71, A85, NAT_1:13;
now__::_thesis:_(_(_1_<=_i_&_i_<_len_fd_&_ex_p1,_p2,_x0_being_set_st_
(_p1_in_PA_&_p2_in_PB_&_f_._i_in_p1_&_x0_in_p1_/\_p2_&_f_._(i_+_1)_in_p2_)_)_or_(_1_<=_i_&_i_=_len_fd_&_ex_p1,_p2,_x0_being_set_st_
(_p1_in_PA_&_p2_in_PB_&_f_._i_in_p1_&_x0_in_p1_/\_p2_&_f_._(i_+_1)_in_p2_)_)_)
percases ( ( 1 <= i & i < len fd ) or ( 1 <= i & i = len fd ) ) by A84, A86, XXREAL_0:1;
case ( 1 <= i & i < len fd ) ; ::_thesis: ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 )
hence  ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 ) by A80; ::_thesis: verum
end;
case ( 1 <= i & i = len fd ) ; ::_thesis: ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 )
hence  ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 ) by A63, A66, A73, A75, A79; ::_thesis: verum
end;
end;
end;
hence  ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 ) ; ::_thesis: verum
end;
 for i being Element of NAT st 1 <= i & i < len f holds
ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 & x0 in p2 & f . (i + 1) in p2 )
proof
let i be Element of NAT ; ::_thesis: ( 1 <= i & i < len f implies ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 & x0 in p2 & f . (i + 1) in p2 ) )
assume  ( 1 <= i & i < len f ) ; ::_thesis: ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 & x0 in p2 & f . (i + 1) in p2 )
then consider p1, p2, x0 being set  such that
A87: ( p1 in PA & p2 in PB & f . i in p1 ) and
A88: x0 in p1 /\ p2 and
A89: f . (i + 1) in p2 by A83;
 ( x0 in p1 & x0 in p2 ) by A88, XBOOLE_0:def_4;
hence  ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 & x0 in p2 & f . (i + 1) in p2 ) by A87, A89; ::_thesis: verum
end;
hence  contradiction by A7, A10, A11, A60, A71, A72, A78, Th21; ::_thesis: verum
end;
then  y in pb by A8, A9, A24, A58, Def2;
then consider y1 being set  such that
A90: y in y1 and
A91: y1 in Cb by A25, TARSKI:def_4;
A92: ex p being Element of PB st
( y1 = p & ex q being set st
( q in Ca & p /\ q <> {} ) ) by A91;
then consider q being set  such that
A93: q in Ca and
A94: y1 /\ q <> {} ;
A95: ex pp being Element of PA st
( q = pp & ex f being FinSequence of Y st
( 1 <= len f & f . 1 = x & f . (len f) in pp & ( for i being Element of NAT st 1 <= i & i < len f holds
ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 ) ) ) ) by A93;
then consider fd being FinSequence of Y such that
A96: 1 <= len fd and
A97: fd . 1 = x and
A98: fd . (len fd) in q and
A99: for i being Element of NAT st 1 <= i & i < len fd holds
ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & fd . i in p1 & x0 in p1 /\ p2 & fd . (i + 1) in p2 ) ;
reconsider y9 = y as Element of Y by A8;
reconsider f = fd ^ <*y9*> as FinSequence of Y ;
 len f = (len fd) + (len <*y9*>) by FINSEQ_1:22;
then A100: len f = (len fd) + 1 by FINSEQ_1:40;
then A101: 1 + 1 <= len f by A96, XREAL_1:6;
A102: f . ((len fd) + 1) in y1 by A90, FINSEQ_1:42;
 y1 meets q by A94, XBOOLE_0:def_7;
then consider z0 being set  such that
A103: ( z0 in y1 & z0 in q ) by XBOOLE_0:3;
A104: z0 in y1 /\ q by A103, XBOOLE_0:def_4;
A105: dom fd = Seg (len fd) by FINSEQ_1:def_3;
A106: for k being Element of NAT st 1 <= k & k <= len fd holds
f . k = fd . k
proof
let k be Element of NAT ; ::_thesis: ( 1 <= k & k <= len fd implies f . k = fd . k )
assume  ( 1 <= k & k <= len fd ) ; ::_thesis: f . k = fd . k
then  k in dom fd by A105, FINSEQ_1:1;
hence  f . k = fd . k by FINSEQ_1:def_7; ::_thesis: verum
end;
then A107: f . (len fd) in q by A96, A98;
A108: for i being Element of NAT st 1 <= i & i < len fd holds
ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 )
proof
let i be Element of NAT ; ::_thesis: ( 1 <= i & i < len fd implies ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 ) )
assume A109: ( 1 <= i & i < len fd ) ; ::_thesis: ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 )
then A110: f . i = fd . i by A106;
 ( 1 <= i + 1 & i + 1 <= len fd ) by A109, NAT_1:13;
then  f . (i + 1) = fd . (i + 1) by A106;
hence  ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 ) by A99, A109, A110; ::_thesis: verum
end;
A111: for i being Element of NAT st 1 <= i & i < len f holds
ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 )
proof
let i be Element of NAT ; ::_thesis: ( 1 <= i & i < len f implies ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 ) )
assume that
A112: 1 <= i and
A113: i < len f ; ::_thesis: ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 )
A114: i <= len fd by A100, A113, NAT_1:13;
now__::_thesis:_(_(_1_<=_i_&_i_<_len_fd_&_ex_p1,_p2,_x0_being_set_st_
(_p1_in_PA_&_p2_in_PB_&_f_._i_in_p1_&_x0_in_p1_/\_p2_&_f_._(i_+_1)_in_p2_)_)_or_(_1_<=_i_&_i_=_len_fd_&_ex_p1,_p2,_x0_being_set_st_
(_p1_in_PA_&_p2_in_PB_&_f_._i_in_p1_&_x0_in_p1_/\_p2_&_f_._(i_+_1)_in_p2_)_)_)
percases ( ( 1 <= i & i < len fd ) or ( 1 <= i & i = len fd ) ) by A112, A114, XXREAL_0:1;
case ( 1 <= i & i < len fd ) ; ::_thesis: ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 )
hence  ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 ) by A108; ::_thesis: verum
end;
case ( 1 <= i & i = len fd ) ; ::_thesis: ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 )
hence  ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 ) by A92, A95, A102, A104, A107; ::_thesis: verum
end;
end;
end;
hence  ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 ) ; ::_thesis: verum
end;
A115: ( (fd ^ <*y9*>) . ((len fd) + 1) = y & 1 <= len f ) by A101, FINSEQ_1:42, XXREAL_0:2;
A116: f . 1 = x by A96, A97, A106;
 for i being Element of NAT st 1 <= i & i < len f holds
ex u being set st
( u in Y & [(f . i),u] in (ERl PA) \/ (ERl PB) & [u,(f . (i + 1))] in (ERl PA) \/ (ERl PB) )
proof
let i be Element of NAT ; ::_thesis: ( 1 <= i & i < len f implies ex u being set st
( u in Y & [(f . i),u] in (ERl PA) \/ (ERl PB) & [u,(f . (i + 1))] in (ERl PA) \/ (ERl PB) ) )
assume  ( 1 <= i & i < len f ) ; ::_thesis: ex u being set st
( u in Y & [(f . i),u] in (ERl PA) \/ (ERl PB) & [u,(f . (i + 1))] in (ERl PA) \/ (ERl PB) )
then consider p1, p2, u being set  such that
A117: p1 in PA and
A118: p2 in PB and
A119: f . i in p1 and
A120: u in p1 /\ p2 and
A121: f . (i + 1) in p2 by A111;
A122: u in p1 by A120, XBOOLE_0:def_4;
A123: u in p2 by A120, XBOOLE_0:def_4;
reconsider x2 = f . i as set ;
reconsider y2 = f . (i + 1) as set ;
A124: [x2,u] in ERl PA by A117, A119, A122, Def6;
A125: [u,y2] in ERl PB by A118, A121, A123, Def6;
 ( ERl PA c= (ERl PA) \/ (ERl PB) & ERl PB c= (ERl PA) \/ (ERl PB) ) by XBOOLE_1:7;
hence  ex u being set st
( u in Y & [(f . i),u] in (ERl PA) \/ (ERl PB) & [u,(f . (i + 1))] in (ERl PA) \/ (ERl PB) ) by A117, A122, A124, A125; ::_thesis: verum
end;
then  [x9,y9] in (ERl PA) "\/" (ERl PB) by A100, A115, A116, Th22;
hence  [x,y] in (ERl PA) "\/" (ERl PB) ; ::_thesis: verum
end;
 for x1, x2 being set st [x1,x2] in (ERl PA) \/ (ERl PB) holds
[x1,x2] in ERl (PA '\/' PB)
proof
let x1, x2 be set ; ::_thesis: ( [x1,x2] in (ERl PA) \/ (ERl PB) implies [x1,x2] in ERl (PA '\/' PB) )
assume  [x1,x2] in (ERl PA) \/ (ERl PB) ; ::_thesis: [x1,x2] in ERl (PA '\/' PB)
then  ( [x1,x2] in ERl PA or [x1,x2] in ERl PB ) by XBOOLE_0:def_3;
then A126: ( ex A being Subset of Y st
( A in PA & x1 in A & x2 in A ) or ex B being Subset of Y st
( B in PB & x1 in B & x2 in B ) ) by Def6;
now__::_thesis:_(_(_x1_in_Y_&_x2_in_Y_&_ex_A_being_Subset_of_Y_st_
(_A_in_PA_&_x1_in_A_&_x2_in_A_)_&_[x1,x2]_in_ERl_(PA_'\/'_PB)_)_or_(_x1_in_Y_&_x2_in_Y_&_ex_B_being_Subset_of_Y_st_
(_B_in_PB_&_x1_in_B_&_x2_in_B_)_&_[x1,x2]_in_ERl_(PA_'\/'_PB)_)_)
percases ( ( x1 in Y & x2 in Y & ex A being Subset of Y st
( A in PA & x1 in A & x2 in A ) ) or ( x1 in Y & x2 in Y & ex B being Subset of Y st
( B in PB & x1 in B & x2 in B ) ) ) by A126;
case ( x1 in Y & x2 in Y & ex A being Subset of Y st
( A in PA & x1 in A & x2 in A ) ) ; ::_thesis: [x1,x2] in ERl (PA '\/' PB)
then consider A being Subset of Y such that
A127: A in PA and
A128: ( x1 in A & x2 in A ) ;
 ex y being set st
( y in PA '\/' PB & A c= y ) by A1, A127, SETFAM_1:def_2;
hence  [x1,x2] in ERl (PA '\/' PB) by A128, Def6; ::_thesis: verum
end;
case ( x1 in Y & x2 in Y & ex B being Subset of Y st
( B in PB & x1 in B & x2 in B ) ) ; ::_thesis: [x1,x2] in ERl (PA '\/' PB)
then consider B being Subset of Y such that
A129: B in PB and
A130: ( x1 in B & x2 in B ) ;
 ex y being set st
( y in PA '\/' PB & B c= y ) by A2, A129, SETFAM_1:def_2;
hence  [x1,x2] in ERl (PA '\/' PB) by A130, Def6; ::_thesis: verum
end;
end;
end;
hence  [x1,x2] in ERl (PA '\/' PB) ; ::_thesis: verum
end;
then  (ERl PA) \/ (ERl PB) c= ERl (PA '\/' PB) by RELAT_1:def_3;
then  (ERl PA) "\/" (ERl PB) c= ERl (PA '\/' PB) by EQREL_1:def_2;
hence  ERl (PA '\/' PB) = (ERl PA) "\/" (ERl PB) by A5, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th24: :: PARTIT1:24
for Y being non empty set
for PA, PB being a_partition of Y holds ERl (PA '/\' PB) = (ERl PA) /\ (ERl PB)
proof
let Y be non empty set ; ::_thesis: for PA, PB being a_partition of Y holds ERl (PA '/\' PB) = (ERl PA) /\ (ERl PB)
let PA, PB be a_partition of Y; ::_thesis: ERl (PA '/\' PB) = (ERl PA) /\ (ERl PB)
A1: PA '>' PA '/\' PB by Th15;
A2: PB '>' PA '/\' PB by Th15;
 for x1, x2 being set holds
( [x1,x2] in ERl (PA '/\' PB) iff [x1,x2] in (ERl PA) /\ (ERl PB) )
proof
let x1, x2 be set ; ::_thesis: ( [x1,x2] in ERl (PA '/\' PB) iff [x1,x2] in (ERl PA) /\ (ERl PB) )
hereby  ::_thesis: ( [x1,x2] in (ERl PA) /\ (ERl PB) implies [x1,x2] in ERl (PA '/\' PB) )
assume  [x1,x2] in ERl (PA '/\' PB) ; ::_thesis: [x1,x2] in (ERl PA) /\ (ERl PB)
then consider C being Subset of Y such that
A3: C in PA '/\' PB and
A4: ( x1 in C & x2 in C ) by Def6;
A5: ex A being set st
( A in PA & C c= A ) by A1, A3, SETFAM_1:def_2;
A6: ex B being set st
( B in PB & C c= B ) by A2, A3, SETFAM_1:def_2;
A7: [x1,x2] in ERl PA by A4, A5, Def6;
 [x1,x2] in ERl PB by A4, A6, Def6;
hence  [x1,x2] in (ERl PA) /\ (ERl PB) by A7, XBOOLE_0:def_4; ::_thesis: verum
end;
assume A8: [x1,x2] in (ERl PA) /\ (ERl PB) ; ::_thesis: [x1,x2] in ERl (PA '/\' PB)
then A9: [x1,x2] in ERl PA by XBOOLE_0:def_4;
A10: [x1,x2] in ERl PB by A8, XBOOLE_0:def_4;
consider A being Subset of Y such that
A11: A in PA and
A12: x1 in A and
A13: x2 in A by A9, Def6;
consider B being Subset of Y such that
A14: B in PB and
A15: x1 in B and
A16: x2 in B by A10, Def6;
A17: A /\ B <> {} by A12, A15, XBOOLE_0:def_4;
consider C being Subset of Y such that
A18: C = A /\ B ;
A19: C in INTERSECTION (PA,PB) by A11, A14, A18, SETFAM_1:def_5;
 not C in {{}} by A17, A18, TARSKI:def_1;
then A20: C in (INTERSECTION (PA,PB)) \ {{}} by A19, XBOOLE_0:def_5;
 ( x1 in C & x2 in C ) by A12, A13, A15, A16, A18, XBOOLE_0:def_4;
hence  [x1,x2] in ERl (PA '/\' PB) by A20, Def6; ::_thesis: verum
end;
hence  ERl (PA '/\' PB) = (ERl PA) /\ (ERl PB) by RELAT_1:def_2; ::_thesis: verum
end;

theorem Th25: :: PARTIT1:25
for Y being non empty set
for PA, PB being a_partition of Y st ERl PA = ERl PB holds
PA = PB
proof
let Y be non empty set ; ::_thesis: for PA, PB being a_partition of Y st ERl PA = ERl PB holds
PA = PB
let PA, PB be a_partition of Y; ::_thesis: ( ERl PA = ERl PB implies PA = PB )
assume  ERl PA = ERl PB ; ::_thesis: PA = PB
then  ( PA '<' PB & PB '<' PA ) by Th20;
hence  PA = PB by Th4; ::_thesis: verum
end;

theorem :: PARTIT1:26
for Y being non empty set
for PA, PB, PC being a_partition of Y holds (PA '\/' PB) '\/' PC = PA '\/' (PB '\/' PC)
proof
let Y be non empty set ; ::_thesis: for PA, PB, PC being a_partition of Y holds (PA '\/' PB) '\/' PC = PA '\/' (PB '\/' PC)
let PA, PB, PC be a_partition of Y; ::_thesis: (PA '\/' PB) '\/' PC = PA '\/' (PB '\/' PC)
ERl ((PA '\/' PB) '\/' PC) = (ERl (PA '\/' PB)) "\/" (ERl PC) by Th23
.= ((ERl PA) "\/" (ERl PB)) "\/" (ERl PC) by Th23
.= (ERl PA) "\/" ((ERl PB) "\/" (ERl PC)) by EQREL_1:13
.= (ERl PA) "\/" (ERl (PB '\/' PC)) by Th23
.= ERl (PA '\/' (PB '\/' PC)) by Th23 ;
hence  (PA '\/' PB) '\/' PC = PA '\/' (PB '\/' PC) by Th25; ::_thesis: verum
end;

theorem :: PARTIT1:27
for Y being non empty set
for PA, PB being a_partition of Y holds PA '/\' (PA '\/' PB) = PA
proof
let Y be non empty set ; ::_thesis: for PA, PB being a_partition of Y holds PA '/\' (PA '\/' PB) = PA
let PA, PB be a_partition of Y; ::_thesis: PA '/\' (PA '\/' PB) = PA
 ( ERl (PA '/\' (PA '\/' PB)) = (ERl PA) /\ (ERl (PA '\/' PB)) & (ERl PA) /\ (ERl (PA '\/' PB)) = (ERl PA) /\ ((ERl PA) "\/" (ERl PB)) ) by Th23, Th24;
hence  PA '/\' (PA '\/' PB) = PA by Th25, EQREL_1:16; ::_thesis: verum
end;

theorem :: PARTIT1:28
for Y being non empty set
for PA, PB being a_partition of Y holds PA '\/' (PA '/\' PB) = PA
proof
let Y be non empty set ; ::_thesis: for PA, PB being a_partition of Y holds PA '\/' (PA '/\' PB) = PA
let PA, PB be a_partition of Y; ::_thesis: PA '\/' (PA '/\' PB) = PA
 ( ERl (PA '\/' (PA '/\' PB)) = (ERl PA) "\/" (ERl (PA '/\' PB)) & (ERl PA) "\/" (ERl (PA '/\' PB)) = (ERl PA) "\/" ((ERl PA) /\ (ERl PB)) ) by Th23, Th24;
hence  PA '\/' (PA '/\' PB) = PA by Th25, EQREL_1:17; ::_thesis: verum
end;

theorem Th29: :: PARTIT1:29
for Y being non empty set
for PA, PB, PC being a_partition of Y st PA '<' PC & PB '<' PC holds
PA '\/' PB '<' PC
proof
let Y be non empty set ; ::_thesis: for PA, PB, PC being a_partition of Y st PA '<' PC & PB '<' PC holds
PA '\/' PB '<' PC
let PA, PB, PC be a_partition of Y; ::_thesis: ( PA '<' PC & PB '<' PC implies PA '\/' PB '<' PC )
assume  ( PA '<' PC & PB '<' PC ) ; ::_thesis: PA '\/' PB '<' PC
then A1: ( ERl PA c= ERl PC & ERl PB c= ERl PC ) by Th20;
A2: ERl (PA '\/' PB) = (ERl PA) "\/" (ERl PB) by Th23;
 (ERl PA) \/ (ERl PB) c= ERl PC by A1, XBOOLE_1:8;
then  (ERl PA) "\/" (ERl PB) c= ERl PC by EQREL_1:def_2;
hence  PA '\/' PB '<' PC by A2, Th20; ::_thesis: verum
end;

theorem :: PARTIT1:30
for Y being non empty set
for PA, PB, PC being a_partition of Y st PA '>' PC & PB '>' PC holds
PA '/\' PB '>' PC
proof
let Y be non empty set ; ::_thesis: for PA, PB, PC being a_partition of Y st PA '>' PC & PB '>' PC holds
PA '/\' PB '>' PC
let PA, PB, PC be a_partition of Y; ::_thesis: ( PA '>' PC & PB '>' PC implies PA '/\' PB '>' PC )
assume  ( PA '>' PC & PB '>' PC ) ; ::_thesis: PA '/\' PB '>' PC
then A1: ( ERl PC c= ERl PA & ERl PC c= ERl PB ) by Th20;
 ERl (PA '/\' PB) = (ERl PA) /\ (ERl PB) by Th24;
then  ERl PC c= ERl (PA '/\' PB) by A1, XBOOLE_1:19;
hence  PA '/\' PB '>' PC by Th20; ::_thesis: verum
end;

notation
let Y be non empty set ;
synonym  %I Y for  SmallestPartition Y;
end;

definition
let Y be non empty set ;
func %O Y ->  a_partition of Y equals :: PARTIT1:def 8
{Y};
correctness
coherence
{Y} is a_partition of Y;
proof
A1: ( {Y} is Subset-Family of Y & union {Y} = Y ) by ZFMISC_1:25, ZFMISC_1:68;
 for A being Subset of Y st A in {Y} holds
( A <> {} & ( for B being Subset of Y holds
( not B in {Y} or A = B or A misses B ) ) )
proof
let A be Subset of Y; ::_thesis: ( A in {Y} implies ( A <> {} & ( for B being Subset of Y holds
( not B in {Y} or A = B or A misses B ) ) ) )
assume A2: A in {Y} ; ::_thesis: ( A <> {} & ( for B being Subset of Y holds
( not B in {Y} or A = B or A misses B ) ) )
then A3: A = Y by TARSKI:def_1;
thus  A <> {} by A2, TARSKI:def_1; ::_thesis: for B being Subset of Y holds
( not B in {Y} or A = B or A misses B )
let B be Subset of Y; ::_thesis: ( not B in {Y} or A = B or A misses B )
assume  B in {Y} ; ::_thesis: ( A = B or A misses B )
hence  ( A = B or A misses B ) by A3, TARSKI:def_1; ::_thesis: verum
end;
hence  {Y} is a_partition of Y by A1, EQREL_1:def_4; ::_thesis: verum
end;
end;

:: deftheorem  defines %O PARTIT1:def_8_:_
 for Y being non empty set holds %O Y = {Y};

theorem :: PARTIT1:31
for Y being non empty set holds %I Y =  {  B where B is Subset of Y : ex x being set st
( B = {x} & x in Y )  }
proof
let Y be non empty set ; ::_thesis: %I Y =  {  B where B is Subset of Y : ex x being set st
( B = {x} & x in Y )  }
set B0 =  {  B where B is Subset of Y : ex x being set st
( B = {x} & x in Y )  }  ;
A1: %I Y c=  {  B where B is Subset of Y : ex x being set st
( B = {x} & x in Y )  }
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in %I Y or a in  {  B where B is Subset of Y : ex x being set st
( B = {x} & x in Y )  }  )
assume  a in %I Y ; ::_thesis: a in  {  B where B is Subset of Y : ex x being set st
( B = {x} & x in Y )  }
then  a in  {  {x} where x is Element of Y : verum  }  by EQREL_1:37;
then consider x being Element of Y such that
A2: a = {x} ;
reconsider y = x as Element of Y ;
reconsider B = {y} as Subset of Y by ZFMISC_1:31;
 a = B by A2;
hence  a in  {  B where B is Subset of Y : ex x being set st
( B = {x} & x in Y )  }  ; ::_thesis: verum
end;
  {  B where B is Subset of Y : ex x being set st
( B = {x} & x in Y )  }  c= %I Y
proof
let x1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not x1 in  {  B where B is Subset of Y : ex x being set st
( B = {x} & x in Y )  }  or x1 in %I Y )
assume  x1 in  {  B where B is Subset of Y : ex x being set st
( B = {x} & x in Y )  }  ; ::_thesis: x1 in %I Y
then  ex B being Subset of Y st
( x1 = B & ex x being set st
( B = {x} & x in Y ) ) ;
then  x1 in  {  {z} where z is Element of Y : verum  }  ;
hence  x1 in %I Y by EQREL_1:37; ::_thesis: verum
end;
hence  %I Y =  {  B where B is Subset of Y : ex x being set st
( B = {x} & x in Y )  }  by A1, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th32: :: PARTIT1:32
for Y being non empty set
for PA being a_partition of Y holds
( %O Y '>' PA & PA '>' %I Y )
proof
let Y be non empty set ; ::_thesis: for PA being a_partition of Y holds
( %O Y '>' PA & PA '>' %I Y )
let PA be a_partition of Y; ::_thesis: ( %O Y '>' PA & PA '>' %I Y )
A1: for a being set st a in PA holds
ex b being set st
( b in %O Y & a c= b )
proof
let a be set ; ::_thesis: ( a in PA implies ex b being set st
( b in %O Y & a c= b ) )
assume A2: a in PA ; ::_thesis: ex b being set st
( b in %O Y & a c= b )
then A3: a c= Y ;
A4: a <> {} by A2, EQREL_1:def_4;
set x = the Element of a;
A5: the Element of a in Y by A2, A4, TARSKI:def_3;
 union (%O Y) = Y by EQREL_1:def_4;
then consider b being set  such that
 the Element of a in b and
A6: b in %O Y by A5, TARSKI:def_4;
 a c= b by A3, A6, TARSKI:def_1;
hence  ex b being set st
( b in %O Y & a c= b ) by A6; ::_thesis: verum
end;
 for a being set st a in %I Y holds
ex b being set st
( b in PA & a c= b )
proof
let a be set ; ::_thesis: ( a in %I Y implies ex b being set st
( b in PA & a c= b ) )
assume A7: a in %I Y ; ::_thesis: ex b being set st
( b in PA & a c= b )
then  a in  {  {x} where x is Element of Y : verum  }  by EQREL_1:37;
then consider x being Element of Y such that
A8: a = {x} ;
A9: a <> {} by A7, EQREL_1:def_4;
set u = the Element of a;
A10: the Element of a = x by A8, TARSKI:def_1;
A11: the Element of a in Y by A7, A9, TARSKI:def_3;
 union PA = Y by EQREL_1:def_4;
then consider b being set  such that
A12: the Element of a in b and
A13: b in PA by A11, TARSKI:def_4;
 a c= b
proof
let x1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not x1 in a or x1 in b )
assume  x1 in a ; ::_thesis: x1 in b
hence  x1 in b by A8, A10, A12, TARSKI:def_1; ::_thesis: verum
end;
hence  ex b being set st
( b in PA & a c= b ) by A13; ::_thesis: verum
end;
hence  ( %O Y '>' PA & PA '>' %I Y ) by A1, SETFAM_1:def_2; ::_thesis: verum
end;

theorem Th33: :: PARTIT1:33
for Y being non empty set holds ERl (%O Y) = nabla Y
proof
let Y be non empty set ; ::_thesis: ERl (%O Y) = nabla Y
 nabla Y c= ERl (%O Y)
proof
let x1, x2 be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [x1,x2] in nabla Y or [x1,x2] in ERl (%O Y) )
assume A1: [x1,x2] in nabla Y ; ::_thesis: [x1,x2] in ERl (%O Y)
A2: Y in %O Y by TARSKI:def_1;
 ( x1 in Y & x2 in Y ) by A1, ZFMISC_1:87;
hence  [x1,x2] in ERl (%O Y) by A2, Def6; ::_thesis: verum
end;
hence  ERl (%O Y) = nabla Y by XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th34: :: PARTIT1:34
for Y being non empty set holds ERl (%I Y) = id Y
proof
let Y be non empty set ; ::_thesis: ERl (%I Y) = id Y
A1: union (%I Y) = Y by EQREL_1:def_4;
A2: ERl (%I Y) c= id Y
proof
let x1, x2 be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [x1,x2] in ERl (%I Y) or [x1,x2] in id Y )
assume  [x1,x2] in ERl (%I Y) ; ::_thesis: [x1,x2] in id Y
then consider a being Subset of Y such that
A3: a in %I Y and
A4: ( x1 in a & x2 in a ) by Def6;
 %I Y =  {  {x} where x is Element of Y : verum  }  by EQREL_1:37;
then consider x being Element of Y such that
A5: a = {x} by A3;
 ( x1 = x & x2 = x ) by A4, A5, TARSKI:def_1;
hence  [x1,x2] in id Y by RELAT_1:def_10; ::_thesis: verum
end;
 id Y c= ERl (%I Y)
proof
let x1, x2 be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [x1,x2] in id Y or [x1,x2] in ERl (%I Y) )
assume A6: [x1,x2] in id Y ; ::_thesis: [x1,x2] in ERl (%I Y)
then A7: x1 in Y by RELAT_1:def_10;
A8: x1 = x2 by A6, RELAT_1:def_10;
 ex y being set st
( x1 in y & y in %I Y ) by A1, A7, TARSKI:def_4;
hence  [x1,x2] in ERl (%I Y) by A8, Def6; ::_thesis: verum
end;
hence  ERl (%I Y) = id Y by A2, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: PARTIT1:35
for Y being non empty set holds %I Y '<' %O Y
proof
let Y be non empty set ; ::_thesis: %I Y '<' %O Y
ERl (%O Y) = nabla Y by Th33
.= [:Y,Y:] ;
then  ERl (%I Y) c= ERl (%O Y) ;
hence  %I Y '<' %O Y by Th20; ::_thesis: verum
end;

theorem :: PARTIT1:36
for Y being non empty set
for PA being a_partition of Y holds
( (%O Y) '\/' PA = %O Y & (%O Y) '/\' PA = PA )
proof
let Y be non empty set ; ::_thesis: for PA being a_partition of Y holds
( (%O Y) '\/' PA = %O Y & (%O Y) '/\' PA = PA )
let PA be a_partition of Y; ::_thesis: ( (%O Y) '\/' PA = %O Y & (%O Y) '/\' PA = PA )
A1: ERl ((%O Y) '\/' PA) = (ERl (%O Y)) "\/" (ERl PA) by Th23;
 ERl (%O Y) = nabla Y by Th33;
then  (ERl (%O Y)) \/ (ERl PA) = ERl (%O Y) by EQREL_1:1;
then  ERl (%O Y) c= (ERl (%O Y)) "\/" (ERl PA) by EQREL_1:def_2;
then A2: %O Y '<' (%O Y) '\/' PA by A1, Th20;
 %O Y '>' PA '\/' (%O Y) by Th32;
hence  (%O Y) '\/' PA = %O Y by A2, Th4; ::_thesis: (%O Y) '/\' PA = PA
 ( ERl ((%O Y) '/\' PA) = (ERl (%O Y)) /\ (ERl PA) & ERl (%O Y) = nabla Y ) by Th24, Th33;
hence  (%O Y) '/\' PA = PA by Th25, XBOOLE_1:28; ::_thesis: verum
end;

theorem :: PARTIT1:37
for Y being non empty set
for PA being a_partition of Y holds
( (%I Y) '\/' PA = PA & (%I Y) '/\' PA = %I Y )
proof
let Y be non empty set ; ::_thesis: for PA being a_partition of Y holds
( (%I Y) '\/' PA = PA & (%I Y) '/\' PA = %I Y )
let PA be a_partition of Y; ::_thesis: ( (%I Y) '\/' PA = PA & (%I Y) '/\' PA = %I Y )
A1: ERl (%I Y) = id Y by Th34;
A2: ( ERl ((%I Y) '\/' PA) = (ERl (%I Y)) "\/" (ERl PA) & (ERl (%I Y)) \/ (ERl PA) c= (ERl (%I Y)) "\/" (ERl PA) ) by Th23, EQREL_1:def_2;
A3: (ERl (%I Y)) \/ (ERl PA) = (id Y) \/ (ERl PA) by Th34;
 %I Y '<' PA by Th32;
then A4: ERl (%I Y) c= ERl PA by Th20;
 for z being set st z in (id Y) \/ (ERl PA) holds
z in ERl PA
proof
let z be set ; ::_thesis: ( z in (id Y) \/ (ERl PA) implies z in ERl PA )
assume A5: z in (id Y) \/ (ERl PA) ; ::_thesis: z in ERl PA
now__::_thesis:_(_(_z_in_id_Y_&_z_in_ERl_PA_)_or_(_z_in_ERl_PA_&_z_in_ERl_PA_)_)
percases ( z in id Y or z in ERl PA ) by A5, XBOOLE_0:def_3;
case z in id Y ; ::_thesis: z in ERl PA
hence  z in ERl PA by A1, A4; ::_thesis: verum
end;
case z in ERl PA ; ::_thesis: z in ERl PA
hence  z in ERl PA ; ::_thesis: verum
end;
end;
end;
hence  z in ERl PA ; ::_thesis: verum
end;
then A6: (id Y) \/ (ERl PA) c= ERl PA by TARSKI:def_3;
 ERl PA c= (id Y) \/ (ERl PA) by XBOOLE_1:7;
then  (id Y) \/ (ERl PA) = ERl PA by A6, XBOOLE_0:def_10;
then A7: PA '<' (%I Y) '\/' PA by A2, A3, Th20;
 %I Y '<' PA by Th32;
then  (%I Y) '\/' PA '<' PA by Th29;
hence  (%I Y) '\/' PA = PA by A7, Th4; ::_thesis: (%I Y) '/\' PA = %I Y
ERl ((%I Y) '/\' PA) = (ERl (%I Y)) /\ (ERl PA) by Th24
.= (id Y) /\ (ERl PA) by Th34
.= id Y by EQREL_1:10
.= ERl (%I Y) by Th34 ;
hence  (%I Y) '/\' PA = %I Y by Th25; ::_thesis: verum
end;