:: PARTIT_2 semantic presentation

begin


definition
let Y be non empty set ;
let G be non empty Subset of (PARTITIONS Y);
:: original: Element
redefine mode Element of G ->  a_partition of Y;
coherence
 for b1 being Element of G holds b1 is a_partition of Y
proof
let p be Element of G; ::_thesis: p is a_partition of Y
thus  p is a_partition of Y by PARTIT1:def_3; ::_thesis: verum
end;
end;

theorem Th1: :: PARTIT_2:1
for Y being non empty set holds '/\' ({} (PARTITIONS Y)) = %O Y
proof
let Y be non empty set ; ::_thesis: '/\' ({} (PARTITIONS Y)) = %O Y
 for x being set holds
( x in %O Y iff ex h being Function ex F being Subset-Family of Y st
( dom h = {} (PARTITIONS Y) & rng h = F & ( for d being set st d in {} (PARTITIONS Y) holds
h . d in d ) & x = Intersect F & x <> {} ) )
proof
let x be set ; ::_thesis: ( x in %O Y iff ex h being Function ex F being Subset-Family of Y st
( dom h = {} (PARTITIONS Y) & rng h = F & ( for d being set st d in {} (PARTITIONS Y) holds
h . d in d ) & x = Intersect F & x <> {} ) )
hereby  ::_thesis: ( ex h being Function ex F being Subset-Family of Y st
( dom h = {} (PARTITIONS Y) & rng h = F & ( for d being set st d in {} (PARTITIONS Y) holds
h . d in d ) & x = Intersect F & x <> {} ) implies x in %O Y )
reconsider h = {} as Function ;
assume  x in %O Y ; ::_thesis: ex h being Function ex F being Element of bool (bool Y) st
( dom h = {} (PARTITIONS Y) & rng h = F & ( for d being set st d in {} (PARTITIONS Y) holds
h . d in d ) & x = Intersect F & x <> {} )
then A1: x in {Y} by PARTIT1:def_8;
take h = h; ::_thesis: ex F being Element of bool (bool Y) st
( dom h = {} (PARTITIONS Y) & rng h = F & ( for d being set st d in {} (PARTITIONS Y) holds
h . d in d ) & x = Intersect F & x <> {} )
take F = {} (bool Y); ::_thesis: ( dom h = {} (PARTITIONS Y) & rng h = F & ( for d being set st d in {} (PARTITIONS Y) holds
h . d in d ) & x = Intersect F & x <> {} )
thus  dom h = {} (PARTITIONS Y) ; ::_thesis: ( rng h = F & ( for d being set st d in {} (PARTITIONS Y) holds
h . d in d ) & x = Intersect F & x <> {} )
thus  rng h = F ; ::_thesis: ( ( for d being set st d in {} (PARTITIONS Y) holds
h . d in d ) & x = Intersect F & x <> {} )
thus  for d being set st d in {} (PARTITIONS Y) holds
h . d in d ; ::_thesis: ( x = Intersect F & x <> {} )
 x = Y by A1, TARSKI:def_1;
hence  x = Intersect F by SETFAM_1:def_9; ::_thesis: x <> {}
thus  x <> {} by A1, TARSKI:def_1; ::_thesis: verum
end;
given h being Function, F being Subset-Family of Y such that A2: ( dom h = {} (PARTITIONS Y) & rng h = F ) and
 for d being set st d in {} (PARTITIONS Y) holds
h . d in d and
A3: x = Intersect F and
 x <> {} ; ::_thesis: x in %O Y
 F = {} by A2, RELAT_1:42;
then  x = Y by A3, SETFAM_1:def_9;
then  x in {Y} by TARSKI:def_1;
hence  x in %O Y by PARTIT1:def_8; ::_thesis: verum
end;
hence  '/\' ({} (PARTITIONS Y)) = %O Y by BVFUNC_2:def_1; ::_thesis: verum
end;

theorem Th2: :: PARTIT_2:2
for Y being non empty set
for R, S being Equivalence_Relation of Y holds R \/ S c= R * S
proof
let Y be non empty set ; ::_thesis: for R, S being Equivalence_Relation of Y holds R \/ S c= R * S
let R, S be Equivalence_Relation of Y; ::_thesis: R \/ S c= R * S
let x, y be Element of Y; :: according to RELSET_1:def_1 ::_thesis: ( not [x,y] in R \/ S or [x,y] in R * S )
assume A1: [x,y] in R \/ S ; ::_thesis: [x,y] in R * S
percases ( [x,y] in R or [x,y] in S ) by A1, XBOOLE_0:def_3;
supposeA2: [x,y] in R ; ::_thesis: [x,y] in R * S
 [y,y] in S by EQREL_1:5;
hence  [x,y] in R * S by A2, RELAT_1:def_8; ::_thesis: verum
end;
supposeA3: [x,y] in S ; ::_thesis: [x,y] in R * S
 [x,x] in R by EQREL_1:5;
hence  [x,y] in R * S by A3, RELAT_1:def_8; ::_thesis: verum
end;
end;
end;

theorem :: PARTIT_2:3
for Y being non empty set
for R being Relation of Y holds R c= nabla Y ;

theorem Th4: :: PARTIT_2:4
for Y being non empty set
for R being Equivalence_Relation of Y holds
( (nabla Y) * R = nabla Y & R * (nabla Y) = nabla Y )
proof
let Y be non empty set ; ::_thesis: for R being Equivalence_Relation of Y holds
( (nabla Y) * R = nabla Y & R * (nabla Y) = nabla Y )
let R be Equivalence_Relation of Y; ::_thesis: ( (nabla Y) * R = nabla Y & R * (nabla Y) = nabla Y )
 (nabla Y) \/ R c= (nabla Y) * R by Th2;
then  nabla Y c= (nabla Y) * R by EQREL_1:1;
hence  (nabla Y) * R = nabla Y by XBOOLE_0:def_10; ::_thesis: R * (nabla Y) = nabla Y
 (nabla Y) \/ R c= R * (nabla Y) by Th2;
then  nabla Y c= R * (nabla Y) by EQREL_1:1;
hence  R * (nabla Y) = nabla Y by XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th5: :: PARTIT_2:5
for Y being non empty set
for P being a_partition of Y
for x, y being Element of Y holds
( [x,y] in ERl P iff x in EqClass (y,P) )
proof
let Y be non empty set ; ::_thesis: for P being a_partition of Y
for x, y being Element of Y holds
( [x,y] in ERl P iff x in EqClass (y,P) )
let P be a_partition of Y; ::_thesis: for x, y being Element of Y holds
( [x,y] in ERl P iff x in EqClass (y,P) )
let x, y be Element of Y; ::_thesis: ( [x,y] in ERl P iff x in EqClass (y,P) )
hereby  ::_thesis: ( x in EqClass (y,P) implies [x,y] in ERl P )
assume  [x,y] in ERl P ; ::_thesis: x in EqClass (y,P)
then  ex A being Subset of Y st
( A in P & x in A & y in A ) by PARTIT1:def_6;
hence  x in EqClass (y,P) by EQREL_1:def_6; ::_thesis: verum
end;
 y in EqClass (y,P) by EQREL_1:def_6;
hence  ( x in EqClass (y,P) implies [x,y] in ERl P ) by PARTIT1:def_6; ::_thesis: verum
end;

theorem :: PARTIT_2:6
for Y being non empty set
for P, Q, R being a_partition of Y st ERl R = (ERl P) * (ERl Q) holds
for x, y being Element of Y holds
( x in EqClass (y,R) iff ex z being Element of Y st
( x in EqClass (z,P) & z in EqClass (y,Q) ) )
proof
let Y be non empty set ; ::_thesis: for P, Q, R being a_partition of Y st ERl R = (ERl P) * (ERl Q) holds
for x, y being Element of Y holds
( x in EqClass (y,R) iff ex z being Element of Y st
( x in EqClass (z,P) & z in EqClass (y,Q) ) )
let P, Q, R be a_partition of Y; ::_thesis: ( ERl R = (ERl P) * (ERl Q) implies for x, y being Element of Y holds
( x in EqClass (y,R) iff ex z being Element of Y st
( x in EqClass (z,P) & z in EqClass (y,Q) ) ) )
assume A1: ERl R = (ERl P) * (ERl Q) ; ::_thesis: for x, y being Element of Y holds
( x in EqClass (y,R) iff ex z being Element of Y st
( x in EqClass (z,P) & z in EqClass (y,Q) ) )
let x, y be Element of Y; ::_thesis: ( x in EqClass (y,R) iff ex z being Element of Y st
( x in EqClass (z,P) & z in EqClass (y,Q) ) )
hereby  ::_thesis: ( ex z being Element of Y st
( x in EqClass (z,P) & z in EqClass (y,Q) ) implies x in EqClass (y,R) )
assume  x in EqClass (y,R) ; ::_thesis: ex z being Element of Y st
( x in EqClass (z,P) & z in EqClass (y,Q) )
then  [x,y] in ERl R by Th5;
then consider z being Element of Y such that
A2: [x,z] in ERl P and
A3: [z,y] in ERl Q by A1, RELSET_1:28;
take z = z; ::_thesis: ( x in EqClass (z,P) & z in EqClass (y,Q) )
thus  x in EqClass (z,P) by A2, Th5; ::_thesis: z in EqClass (y,Q)
thus  z in EqClass (y,Q) by A3, Th5; ::_thesis: verum
end;
given z being Element of Y such that A4: ( x in EqClass (z,P) & z in EqClass (y,Q) ) ; ::_thesis: x in EqClass (y,R)
 ( [x,z] in ERl P & [z,y] in ERl Q ) by A4, Th5;
then  [x,y] in ERl R by A1, RELAT_1:def_8;
hence  x in EqClass (y,R) by Th5; ::_thesis: verum
end;

theorem Th7: :: PARTIT_2:7
for R, S being Relation
for Y being set st R is_reflexive_in Y & S is_reflexive_in Y holds
R * S is_reflexive_in Y
proof
let R, S be Relation; ::_thesis: for Y being set st R is_reflexive_in Y & S is_reflexive_in Y holds
R * S is_reflexive_in Y
let Y be set ; ::_thesis: ( R is_reflexive_in Y & S is_reflexive_in Y implies R * S is_reflexive_in Y )
assume A1: ( R is_reflexive_in Y & S is_reflexive_in Y ) ; ::_thesis: R * S is_reflexive_in Y
let x be set ; :: according to RELAT_2:def_1 ::_thesis: ( not x in Y or [x,x] in R * S )
assume  x in Y ; ::_thesis: [x,x] in R * S
then  ( [x,x] in R & [x,x] in S ) by A1, RELAT_2:def_1;
hence  [x,x] in R * S by RELAT_1:def_8; ::_thesis: verum
end;

theorem Th8: :: PARTIT_2:8
for R being Relation
for Y being set st R is_reflexive_in Y holds
Y c= field R
proof
let R be Relation; ::_thesis: for Y being set st R is_reflexive_in Y holds
Y c= field R
let Y be set ; ::_thesis: ( R is_reflexive_in Y implies Y c= field R )
assume A1: R is_reflexive_in Y ; ::_thesis: Y c= field R
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Y or x in field R )
assume  x in Y ; ::_thesis: x in field R
then  [x,x] in R by A1, RELAT_2:def_1;
hence  x in field R by RELAT_1:15; ::_thesis: verum
end;

theorem Th9: :: PARTIT_2:9
for Y being set
for R being Relation of Y st R is_reflexive_in Y holds
Y = field R
proof
let Y be set ; ::_thesis: for R being Relation of Y st R is_reflexive_in Y holds
Y = field R
let R be Relation of Y; ::_thesis: ( R is_reflexive_in Y implies Y = field R )
assume  R is_reflexive_in Y ; ::_thesis: Y = field R
hence  Y c= field R by Th8; :: according to XBOOLE_0:def_10 ::_thesis: field R c= Y
 field R c= Y \/ Y by RELSET_1:8;
hence  field R c= Y ; ::_thesis: verum
end;

theorem :: PARTIT_2:10
for Y being non empty set
for R, S being Equivalence_Relation of Y st R * S = S * R holds
R * S is Equivalence_Relation of Y
proof
let Y be non empty set ; ::_thesis: for R, S being Equivalence_Relation of Y st R * S = S * R holds
R * S is Equivalence_Relation of Y
let R, S be Equivalence_Relation of Y; ::_thesis: ( R * S = S * R implies R * S is Equivalence_Relation of Y )
assume A1: R * S = S * R ; ::_thesis: R * S is Equivalence_Relation of Y
A2: field S = Y by ORDERS_1:12;
then A3: S is_reflexive_in Y by RELAT_2:def_9;
A4: field R = Y by ORDERS_1:12;
then  R is_reflexive_in Y by RELAT_2:def_9;
then  R * S is_reflexive_in Y by A3, Th7;
then A5: ( field (R * S) = Y & dom (R * S) = Y ) by ORDERS_1:13;
A6: R * S is_symmetric_in Y
proof
A7: S is_symmetric_in Y by A2, RELAT_2:def_11;
let x, y be set ; :: according to RELAT_2:def_3 ::_thesis: ( not x in Y or not y in Y or not [x,y] in R * S or [y,x] in R * S )
assume that
A8: x in Y and
A9: y in Y ; ::_thesis: ( not [x,y] in R * S or [y,x] in R * S )
assume  [x,y] in R * S ; ::_thesis: [y,x] in R * S
then consider z being set  such that
A10: [x,z] in R and
A11: [z,y] in S by RELAT_1:def_8;
 z in field S by A11, RELAT_1:15;
then A12: [y,z] in S by A2, A7, A9, A11, RELAT_2:def_3;
A13: R is_symmetric_in Y by A4, RELAT_2:def_11;
 z in field R by A10, RELAT_1:15;
then  [z,x] in R by A4, A13, A8, A10, RELAT_2:def_3;
hence  [y,x] in R * S by A1, A12, RELAT_1:def_8; ::_thesis: verum
end;
A14: ( R * R c= R & S * S c= S ) by RELAT_2:27;
(R * S) * (R * S) = ((R * S) * R) * S by RELAT_1:36
.= (R * (R * S)) * S by A1, RELAT_1:36
.= ((R * R) * S) * S by RELAT_1:36
.= (R * R) * (S * S) by RELAT_1:36 ;
then  (R * S) * (R * S) c= R * S by A14, RELAT_1:31;
hence  R * S is Equivalence_Relation of Y by A5, A6, PARTFUN1:def_2, RELAT_2:27, RELAT_2:def_11; ::_thesis: verum
end;

begin

theorem Th11: :: PARTIT_2:11
for Y being non empty set
for a, b being Function of Y,BOOLEAN st a '<' b holds
'not' b '<' 'not' a
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN st a '<' b holds
'not' b '<' 'not' a
let a, b be Function of Y,BOOLEAN; ::_thesis: ( a '<' b implies 'not' b '<' 'not' a )
assume A1: a '<' b ; ::_thesis: 'not' b '<' 'not' a
let x be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ('not' b) . x = TRUE or ('not' a) . x = TRUE )
assume A2: ('not' b) . x = TRUE ; ::_thesis: ('not' a) . x = TRUE
b . x = ('not' ('not' b)) . x
.= 'not' TRUE by A2, MARGREL1:def_19
.= FALSE ;
then  a . x <> TRUE by A1, BVFUNC_1:def_12;
then  a . x = FALSE by XBOOLEAN:def_3;
hence ('not' a) . x = 'not' FALSE by MARGREL1:def_19
.= TRUE ;
::_thesis: verum
end;

theorem Th12: :: PARTIT_2:12
for Y being non empty set
for a, b being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for P being a_partition of Y st a '<' b holds
All (a,P,G) '<' All (b,P,G)
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for P being a_partition of Y st a '<' b holds
All (a,P,G) '<' All (b,P,G)
let a, b be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y)
for P being a_partition of Y st a '<' b holds
All (a,P,G) '<' All (b,P,G)
let G be Subset of (PARTITIONS Y); ::_thesis: for P being a_partition of Y st a '<' b holds
All (a,P,G) '<' All (b,P,G)
let P be a_partition of Y; ::_thesis: ( a '<' b implies All (a,P,G) '<' All (b,P,G) )
assume A1: a '<' b ; ::_thesis: All (a,P,G) '<' All (b,P,G)
let x be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (All (a,P,G)) . x = TRUE or (All (b,P,G)) . x = TRUE )
assume A2: (All (a,P,G)) . x = TRUE ; ::_thesis: (All (b,P,G)) . x = TRUE
A3: All (a,P,G) = B_INF (a,(CompF (P,G))) by BVFUNC_2:def_9;
A4: for y being Element of Y st y in EqClass (x,(CompF (P,G))) holds
b . y = TRUE
proof
let y be Element of Y; ::_thesis: ( y in EqClass (x,(CompF (P,G))) implies b . y = TRUE )
assume  y in EqClass (x,(CompF (P,G))) ; ::_thesis: b . y = TRUE
then  a . y = TRUE by A3, A2, BVFUNC_1:def_16;
hence  b . y = TRUE by A1, BVFUNC_1:def_12; ::_thesis: verum
end;
 All (b,P,G) = B_INF (b,(CompF (P,G))) by BVFUNC_2:def_9;
hence  (All (b,P,G)) . x = TRUE by A4, BVFUNC_1:def_16; ::_thesis: verum
end;

theorem :: PARTIT_2:13
for Y being non empty set
for a, b being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for P being a_partition of Y st a '<' b holds
Ex (a,P,G) '<' Ex (b,P,G)
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for P being a_partition of Y st a '<' b holds
Ex (a,P,G) '<' Ex (b,P,G)
let a, b be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y)
for P being a_partition of Y st a '<' b holds
Ex (a,P,G) '<' Ex (b,P,G)
let G be Subset of (PARTITIONS Y); ::_thesis: for P being a_partition of Y st a '<' b holds
Ex (a,P,G) '<' Ex (b,P,G)
let P be a_partition of Y; ::_thesis: ( a '<' b implies Ex (a,P,G) '<' Ex (b,P,G) )
A1: Ex (b,P,G) = Ex (('not' ('not' b)),P,G)
.= 'not' (All (('not' b),P,G)) by BVFUNC_2:18 ;
assume  a '<' b ; ::_thesis: Ex (a,P,G) '<' Ex (b,P,G)
then  'not' b '<' 'not' a by Th11;
then A2: All (('not' b),P,G) '<' All (('not' a),P,G) by Th12;
Ex (a,P,G) = Ex (('not' ('not' a)),P,G)
.= 'not' (All (('not' a),P,G)) by BVFUNC_2:18 ;
hence  Ex (a,P,G) '<' Ex (b,P,G) by A1, A2, Th11; ::_thesis: verum
end;

begin

Lm1:  for Y being non empty set
for G being Subset of (PARTITIONS Y) st G is independent holds
for P, Q being Subset of (PARTITIONS Y) st P c= G & Q c= G holds
(ERl ('/\' P)) * (ERl ('/\' Q)) c= (ERl ('/\' Q)) * (ERl ('/\' P))
proof
let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y) st G is independent holds
for P, Q being Subset of (PARTITIONS Y) st P c= G & Q c= G holds
(ERl ('/\' P)) * (ERl ('/\' Q)) c= (ERl ('/\' Q)) * (ERl ('/\' P))
let G be Subset of (PARTITIONS Y); ::_thesis: ( G is independent implies for P, Q being Subset of (PARTITIONS Y) st P c= G & Q c= G holds
(ERl ('/\' P)) * (ERl ('/\' Q)) c= (ERl ('/\' Q)) * (ERl ('/\' P)) )
assume A1: G is independent ; ::_thesis: for P, Q being Subset of (PARTITIONS Y) st P c= G & Q c= G holds
(ERl ('/\' P)) * (ERl ('/\' Q)) c= (ERl ('/\' Q)) * (ERl ('/\' P))
let P, Q be Subset of (PARTITIONS Y); ::_thesis: ( P c= G & Q c= G implies (ERl ('/\' P)) * (ERl ('/\' Q)) c= (ERl ('/\' Q)) * (ERl ('/\' P)) )
assume that
A2: P c= G and
A3: Q c= G ; ::_thesis: (ERl ('/\' P)) * (ERl ('/\' Q)) c= (ERl ('/\' Q)) * (ERl ('/\' P))
percases ( P = {} or Q = {} or ( P <> {} & Q <> {} ) ) ;
suppose P = {} ; ::_thesis: (ERl ('/\' P)) * (ERl ('/\' Q)) c= (ERl ('/\' Q)) * (ERl ('/\' P))
then  P = {} (PARTITIONS Y) ;
then (ERl ('/\' Q)) * (ERl ('/\' P)) = (ERl ('/\' Q)) * (ERl (%O Y)) by Th1
.= (ERl ('/\' Q)) * (nabla Y) by PARTIT1:33
.= nabla Y by Th4 ;
hence  (ERl ('/\' P)) * (ERl ('/\' Q)) c= (ERl ('/\' Q)) * (ERl ('/\' P)) ; ::_thesis: verum
end;
suppose Q = {} ; ::_thesis: (ERl ('/\' P)) * (ERl ('/\' Q)) c= (ERl ('/\' Q)) * (ERl ('/\' P))
then  Q = {} (PARTITIONS Y) ;
then (ERl ('/\' Q)) * (ERl ('/\' P)) = (ERl (%O Y)) * (ERl ('/\' P)) by Th1
.= (nabla Y) * (ERl ('/\' P)) by PARTIT1:33
.= nabla Y by Th4 ;
hence  (ERl ('/\' P)) * (ERl ('/\' Q)) c= (ERl ('/\' Q)) * (ERl ('/\' P)) ; ::_thesis: verum
end;
supposeA4: ( P <> {} & Q <> {} ) ; ::_thesis: (ERl ('/\' P)) * (ERl ('/\' Q)) c= (ERl ('/\' Q)) * (ERl ('/\' P))
then reconsider G9 = G as non empty Subset of (PARTITIONS Y) by A2;
let x, y be Element of Y; :: according to RELSET_1:def_1 ::_thesis: ( not [x,y] in (ERl ('/\' P)) * (ERl ('/\' Q)) or [x,y] in (ERl ('/\' Q)) * (ERl ('/\' P)) )
assume  [x,y] in (ERl ('/\' P)) * (ERl ('/\' Q)) ; ::_thesis: [x,y] in (ERl ('/\' Q)) * (ERl ('/\' P))
then consider z being Element of Y such that
A5: [x,z] in ERl ('/\' P) and
A6: [z,y] in ERl ('/\' Q) by RELSET_1:28;
consider A being Subset of Y such that
A7: A in '/\' P and
A8: x in A and
A9: z in A by A5, PARTIT1:def_6;
consider B being Subset of Y such that
A10: B in '/\' Q and
A11: z in B and
A12: y in B by A6, PARTIT1:def_6;
consider hQ being Function, FQ being Subset-Family of Y such that
A13: ( dom hQ = Q & rng hQ = FQ ) and
A14: for d being set st d in Q holds
hQ . d in d and
A15: B = Intersect FQ and
 B <> {} by A10, BVFUNC_2:def_1;
consider hP being Function, FP being Subset-Family of Y such that
A16: ( dom hP = P & rng hP = FP ) and
A17: for d being set st d in P holds
hP . d in d and
A18: A = Intersect FP and
 A <> {} by A7, BVFUNC_2:def_1;
reconsider P = P, Q = Q as non empty Subset of (PARTITIONS Y) by A4;
deffunc H1( Element of P) ->  Element of $1 = EqClass (y,$1);
consider hP9 being Function of P,(bool Y) such that
A19: for p being Element of P holds hP9 . p = H1(p) from FUNCT_2:sch_4();
deffunc H2( Element of Q) ->  Element of $1 = EqClass (x,$1);
consider hQ9 being Function of Q,(bool Y) such that
A20: for p being Element of Q holds hQ9 . p = H2(p) from FUNCT_2:sch_4();
deffunc H3( set ) ->  set = $1;
A21: for d being Element of G9 holds bool Y meets H3(d)
proof
let d be Element of G9; ::_thesis: bool Y meets H3(d)
 d meets d ;
hence  bool Y meets d by XBOOLE_1:63; ::_thesis: verum
end;
consider h9 being Function of G9,(bool Y) such that
A22: for d being Element of G9 holds h9 . d in H3(d) from FUNCT_2:sch_10(A21);
set h = (h9 +* hP9) +* hQ9;
A23: dom hQ9 = Q by FUNCT_2:def_1;
A24: dom hP9 = P by FUNCT_2:def_1;
A25: for d being set st d in P holds
((h9 +* hP9) +* hQ9) . d = hP9 . d
proof
let d be set ; ::_thesis: ( d in P implies ((h9 +* hP9) +* hQ9) . d = hP9 . d )
assume A26: d in P ; ::_thesis: ((h9 +* hP9) +* hQ9) . d = hP9 . d
then reconsider d9 = d as Element of P ;
percases ( d in Q or not d in Q ) ;
supposeA27: d in Q ; ::_thesis: ((h9 +* hP9) +* hQ9) . d = hP9 . d
then A28: hQ . d in FQ by A13, FUNCT_1:def_3;
then A29: y in hQ . d by A12, A15, SETFAM_1:43;
A30: z in hQ . d by A11, A15, A28, SETFAM_1:43;
A31: hQ . d in d by A14, A27;
A32: hP . d in FP by A16, A26, FUNCT_1:def_3;
then A33: x in hP . d by A8, A18, SETFAM_1:43;
A34: z in hP . d by A9, A18, A32, SETFAM_1:43;
A35: hP . d in d by A17, A26;
thus ((h9 +* hP9) +* hQ9) . d = hQ9 . d by A23, A27, FUNCT_4:13
.= EqClass (x,d9) by A20, A27
.= hP . d by A35, A33, EQREL_1:def_6
.= EqClass (z,d9) by A35, A34, EQREL_1:def_6
.= hQ . d by A31, A30, EQREL_1:def_6
.= EqClass (y,d9) by A31, A29, EQREL_1:def_6
.= hP9 . d by A19 ; ::_thesis: verum
end;
suppose not d in Q ; ::_thesis: ((h9 +* hP9) +* hQ9) . d = hP9 . d
hence ((h9 +* hP9) +* hQ9) . d = (h9 +* hP9) . d by A23, FUNCT_4:11
.= hP9 . d by A24, A26, FUNCT_4:13 ;
::_thesis: verum
end;
end;
end;
reconsider FP9 = rng hP9, FQ9 = rng hQ9 as Subset-Family of Y ;
set A9 = Intersect FP9;
set B9 = Intersect FQ9;
 for a being set st a in FP9 holds
y in a
proof
let a be set ; ::_thesis: ( a in FP9 implies y in a )
assume  a in FP9 ; ::_thesis: y in a
then consider b being set  such that
A36: b in dom hP9 and
A37: hP9 . b = a by FUNCT_1:def_3;
reconsider b = b as Element of P by A36;
 a = EqClass (y,b) by A19, A37;
hence  y in a by EQREL_1:def_6; ::_thesis: verum
end;
then A38: y in Intersect FP9 by SETFAM_1:43;
 for a being set st a in FQ9 holds
x in a
proof
let a be set ; ::_thesis: ( a in FQ9 implies x in a )
assume  a in FQ9 ; ::_thesis: x in a
then consider b being set  such that
A39: b in dom hQ9 and
A40: hQ9 . b = a by FUNCT_1:def_3;
reconsider b = b as Element of Q by A39;
 a = EqClass (x,b) by A20, A40;
hence  x in a by EQREL_1:def_6; ::_thesis: verum
end;
then A41: x in Intersect FQ9 by SETFAM_1:43;
A42: for d being set st d in Q holds
hQ9 . d in d
proof
let d be set ; ::_thesis: ( d in Q implies hQ9 . d in d )
assume  d in Q ; ::_thesis: hQ9 . d in d
then reconsider d = d as Element of Q ;
 hQ9 . d = EqClass (x,d) by A20;
hence  hQ9 . d in d ; ::_thesis: verum
end;
 rng (h9 +* hP9) c= (rng h9) \/ (rng hP9) by FUNCT_4:17;
then  rng (h9 +* hP9) c= bool Y by XBOOLE_1:1;
then  ( rng ((h9 +* hP9) +* hQ9) c= (rng (h9 +* hP9)) \/ (rng hQ9) & (rng (h9 +* hP9)) \/ (rng hQ9) c= bool Y ) by FUNCT_4:17, XBOOLE_1:8;
then reconsider F = rng ((h9 +* hP9) +* hQ9) as Subset-Family of Y by XBOOLE_1:1;
A43: dom ((h9 +* hP9) +* hQ9) = (dom (h9 +* hP9)) \/ Q by A23, FUNCT_4:def_1
.= ((dom h9) \/ P) \/ Q by A24, FUNCT_4:def_1
.= (G \/ P) \/ Q by FUNCT_2:def_1
.= G \/ Q by A2, XBOOLE_1:12
.= G by A3, XBOOLE_1:12 ;
A44: for d being set st d in P holds
hP9 . d in d
proof
let d be set ; ::_thesis: ( d in P implies hP9 . d in d )
assume  d in P ; ::_thesis: hP9 . d in d
then reconsider d = d as Element of P ;
 hP9 . d = EqClass (y,d) by A19;
hence  hP9 . d in d ; ::_thesis: verum
end;
 for d being set st d in G holds
((h9 +* hP9) +* hQ9) . d in d
proof
let d be set ; ::_thesis: ( d in G implies ((h9 +* hP9) +* hQ9) . d in d )
assume A45: d in G ; ::_thesis: ((h9 +* hP9) +* hQ9) . d in d
G = (P \/ Q) \/ G by A2, A3, XBOOLE_1:8, XBOOLE_1:12
.= (G \ (P \/ Q)) \/ (P \/ Q) by XBOOLE_1:39 ;
then A46: ( d in G \ (P \/ Q) or d in P \/ Q ) by A45, XBOOLE_0:def_3;
percases ( d in Q or d in P or d in G \ (P \/ Q) ) by A46, XBOOLE_0:def_3;
supposeA47: d in Q ; ::_thesis: ((h9 +* hP9) +* hQ9) . d in d
then  ((h9 +* hP9) +* hQ9) . d = hQ9 . d by A23, FUNCT_4:13;
hence  ((h9 +* hP9) +* hQ9) . d in d by A42, A47; ::_thesis: verum
end;
supposeA48: d in P ; ::_thesis: ((h9 +* hP9) +* hQ9) . d in d
then  ((h9 +* hP9) +* hQ9) . d = hP9 . d by A25;
hence  ((h9 +* hP9) +* hQ9) . d in d by A44, A48; ::_thesis: verum
end;
supposeA49: d in G \ (P \/ Q) ; ::_thesis: ((h9 +* hP9) +* hQ9) . d in d
then  not d in P \/ Q by XBOOLE_0:def_5;
then  ( (h9 +* hP9) +* hQ9 = h9 +* (hP9 +* hQ9) & not d in dom (hP9 +* hQ9) ) by A24, A23, FUNCT_4:14, FUNCT_4:def_1;
then A50: ((h9 +* hP9) +* hQ9) . d = h9 . d by FUNCT_4:11;
 d in G by A49, XBOOLE_0:def_5;
hence  ((h9 +* hP9) +* hQ9) . d in d by A22, A50; ::_thesis: verum
end;
end;
end;
then  Intersect F <> {} by A1, A43, BVFUNC_2:def_5;
then consider t being Element of Y such that
A51: t in Intersect F by SUBSET_1:4;
 for a being set st a in FP9 holds
t in a
proof
let a be set ; ::_thesis: ( a in FP9 implies t in a )
assume  a in FP9 ; ::_thesis: t in a
then consider b being set  such that
A52: b in dom hP9 and
A53: hP9 . b = a by FUNCT_1:def_3;
 hP9 . b = ((h9 +* hP9) +* hQ9) . b by A25, A52;
then  a in F by A2, A24, A43, A52, A53, FUNCT_1:def_3;
hence  t in a by A51, SETFAM_1:43; ::_thesis: verum
end;
then A54: t in Intersect FP9 by SETFAM_1:43;
then  Intersect FP9 in '/\' P by A44, A24, BVFUNC_2:def_1;
then A55: [t,y] in ERl ('/\' P) by A38, A54, PARTIT1:def_6;
 for a being set st a in FQ9 holds
t in a
proof
let a be set ; ::_thesis: ( a in FQ9 implies t in a )
assume  a in FQ9 ; ::_thesis: t in a
then consider b being set  such that
A56: b in dom hQ9 and
A57: hQ9 . b = a by FUNCT_1:def_3;
reconsider b = b as Element of Q by A56;
 hQ9 . b = ((h9 +* hP9) +* hQ9) . b by A56, FUNCT_4:13;
then  a in F by A3, A23, A43, A56, A57, FUNCT_1:def_3;
hence  t in a by A51, SETFAM_1:43; ::_thesis: verum
end;
then A58: t in Intersect FQ9 by SETFAM_1:43;
then  Intersect FQ9 in '/\' Q by A42, A23, BVFUNC_2:def_1;
then  [x,t] in ERl ('/\' Q) by A41, A58, PARTIT1:def_6;
hence  [x,y] in (ERl ('/\' Q)) * (ERl ('/\' P)) by A55, RELSET_1:28; ::_thesis: verum
end;
end;
end;

theorem Th14: :: PARTIT_2:14
for Y being non empty set
for G being Subset of (PARTITIONS Y) st G is independent holds
for P, Q being Subset of (PARTITIONS Y) st P c= G & Q c= G holds
(ERl ('/\' P)) * (ERl ('/\' Q)) = (ERl ('/\' Q)) * (ERl ('/\' P))
proof
let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y) st G is independent holds
for P, Q being Subset of (PARTITIONS Y) st P c= G & Q c= G holds
(ERl ('/\' P)) * (ERl ('/\' Q)) = (ERl ('/\' Q)) * (ERl ('/\' P))
let G be Subset of (PARTITIONS Y); ::_thesis: ( G is independent implies for P, Q being Subset of (PARTITIONS Y) st P c= G & Q c= G holds
(ERl ('/\' P)) * (ERl ('/\' Q)) = (ERl ('/\' Q)) * (ERl ('/\' P)) )
assume A1: G is independent ; ::_thesis: for P, Q being Subset of (PARTITIONS Y) st P c= G & Q c= G holds
(ERl ('/\' P)) * (ERl ('/\' Q)) = (ERl ('/\' Q)) * (ERl ('/\' P))
let P, Q be Subset of (PARTITIONS Y); ::_thesis: ( P c= G & Q c= G implies (ERl ('/\' P)) * (ERl ('/\' Q)) = (ERl ('/\' Q)) * (ERl ('/\' P)) )
assume  ( P c= G & Q c= G ) ; ::_thesis: (ERl ('/\' P)) * (ERl ('/\' Q)) = (ERl ('/\' Q)) * (ERl ('/\' P))
then  ( (ERl ('/\' P)) * (ERl ('/\' Q)) c= (ERl ('/\' Q)) * (ERl ('/\' P)) & (ERl ('/\' Q)) * (ERl ('/\' P)) c= (ERl ('/\' P)) * (ERl ('/\' Q)) ) by A1, Lm1;
hence  (ERl ('/\' P)) * (ERl ('/\' Q)) = (ERl ('/\' Q)) * (ERl ('/\' P)) by XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th15: :: PARTIT_2:15
for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for P, Q being a_partition of Y st G is independent holds
All ((All (a,P,G)),Q,G) = All ((All (a,Q,G)),P,G)
proof
let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for P, Q being a_partition of Y st G is independent holds
All ((All (a,P,G)),Q,G) = All ((All (a,Q,G)),P,G)
let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y)
for P, Q being a_partition of Y st G is independent holds
All ((All (a,P,G)),Q,G) = All ((All (a,Q,G)),P,G)
let G be Subset of (PARTITIONS Y); ::_thesis: for P, Q being a_partition of Y st G is independent holds
All ((All (a,P,G)),Q,G) = All ((All (a,Q,G)),P,G)
let P, Q be a_partition of Y; ::_thesis: ( G is independent implies All ((All (a,P,G)),Q,G) = All ((All (a,Q,G)),P,G) )
set A = G \ {P};
set B = G \ {Q};
A1: CompF (P,G) = '/\' (G \ {P}) by BVFUNC_2:def_7;
A2: ( G \ {P} c= G & G \ {Q} c= G ) by XBOOLE_1:36;
A3: CompF (Q,G) = '/\' (G \ {Q}) by BVFUNC_2:def_7;
assume  G is independent ; ::_thesis: All ((All (a,P,G)),Q,G) = All ((All (a,Q,G)),P,G)
then A4: (ERl ('/\' (G \ {P}))) * (ERl ('/\' (G \ {Q}))) = (ERl ('/\' (G \ {Q}))) * (ERl ('/\' (G \ {P}))) by A2, Th14;
A5: for y being Element of Y holds
( ( ( for x being Element of Y st x in EqClass (y,(CompF (Q,G))) holds
(B_INF (a,(CompF (P,G)))) . x = TRUE ) implies (B_INF ((B_INF (a,(CompF (Q,G)))),(CompF (P,G)))) . y = TRUE ) & ( ex x being Element of Y st
( x in EqClass (y,(CompF (Q,G))) & not (B_INF (a,(CompF (P,G)))) . x = TRUE ) implies (B_INF ((B_INF (a,(CompF (Q,G)))),(CompF (P,G)))) . y = FALSE ) )
proof
let y be Element of Y; ::_thesis: ( ( ( for x being Element of Y st x in EqClass (y,(CompF (Q,G))) holds
(B_INF (a,(CompF (P,G)))) . x = TRUE ) implies (B_INF ((B_INF (a,(CompF (Q,G)))),(CompF (P,G)))) . y = TRUE ) & ( ex x being Element of Y st
( x in EqClass (y,(CompF (Q,G))) & not (B_INF (a,(CompF (P,G)))) . x = TRUE ) implies (B_INF ((B_INF (a,(CompF (Q,G)))),(CompF (P,G)))) . y = FALSE ) )
hereby  ::_thesis: ( ex x being Element of Y st
( x in EqClass (y,(CompF (Q,G))) & not (B_INF (a,(CompF (P,G)))) . x = TRUE ) implies (B_INF ((B_INF (a,(CompF (Q,G)))),(CompF (P,G)))) . y = FALSE )
assume A6: for x being Element of Y st x in EqClass (y,(CompF (Q,G))) holds
(B_INF (a,(CompF (P,G)))) . x = TRUE ; ::_thesis: (B_INF ((B_INF (a,(CompF (Q,G)))),(CompF (P,G)))) . y = TRUE
 for x being Element of Y st x in EqClass (y,(CompF (P,G))) holds
(B_INF (a,(CompF (Q,G)))) . x = TRUE
proof
let x be Element of Y; ::_thesis: ( x in EqClass (y,(CompF (P,G))) implies (B_INF (a,(CompF (Q,G)))) . x = TRUE )
assume  x in EqClass (y,(CompF (P,G))) ; ::_thesis: (B_INF (a,(CompF (Q,G)))) . x = TRUE
then A7: [x,y] in ERl ('/\' (G \ {P})) by A1, Th5;
 for z being Element of Y st z in EqClass (x,(CompF (Q,G))) holds
a . z = TRUE
proof
let z be Element of Y; ::_thesis: ( z in EqClass (x,(CompF (Q,G))) implies a . z = TRUE )
assume  z in EqClass (x,(CompF (Q,G))) ; ::_thesis: a . z = TRUE
then  [z,x] in ERl ('/\' (G \ {Q})) by A3, Th5;
then  [z,y] in (ERl ('/\' (G \ {P}))) * (ERl ('/\' (G \ {Q}))) by A4, A7, RELAT_1:def_8;
then consider u being set  such that
A8: [z,u] in ERl ('/\' (G \ {P})) and
A9: [u,y] in ERl ('/\' (G \ {Q})) by RELAT_1:def_8;
 u in field (ERl ('/\' (G \ {Q}))) by A9, RELAT_1:15;
then reconsider u = u as Element of Y by ORDERS_1:12;
 u in EqClass (y,(CompF (Q,G))) by A3, A9, Th5;
then A10: (B_INF (a,(CompF (P,G)))) . u <> FALSE by A6;
 z in EqClass (u,(CompF (P,G))) by A1, A8, Th5;
hence  a . z = TRUE by A10, BVFUNC_1:def_16; ::_thesis: verum
end;
hence  (B_INF (a,(CompF (Q,G)))) . x = TRUE by BVFUNC_1:def_16; ::_thesis: verum
end;
hence  (B_INF ((B_INF (a,(CompF (Q,G)))),(CompF (P,G)))) . y = TRUE by BVFUNC_1:def_16; ::_thesis: verum
end;
given x being Element of Y such that A11: x in EqClass (y,(CompF (Q,G))) and
A12: (B_INF (a,(CompF (P,G)))) . x <> TRUE ; ::_thesis: (B_INF ((B_INF (a,(CompF (Q,G)))),(CompF (P,G)))) . y = FALSE
consider z being Element of Y such that
A13: z in EqClass (x,(CompF (P,G))) and
A14: a . z <> TRUE by A12, BVFUNC_1:def_16;
A15: [x,y] in ERl ('/\' (G \ {Q})) by A3, A11, Th5;
 [z,x] in ERl ('/\' (G \ {P})) by A1, A13, Th5;
then  [z,y] in (ERl ('/\' (G \ {Q}))) * (ERl ('/\' (G \ {P}))) by A4, A15, RELAT_1:def_8;
then consider u being set  such that
A16: [z,u] in ERl ('/\' (G \ {Q})) and
A17: [u,y] in ERl ('/\' (G \ {P})) by RELAT_1:def_8;
 u in field (ERl ('/\' (G \ {Q}))) by A16, RELAT_1:15;
then reconsider u = u as Element of Y by ORDERS_1:12;
 z in EqClass (u,(CompF (Q,G))) by A3, A16, Th5;
then A18: (B_INF (a,(CompF (Q,G)))) . u = FALSE by A14, BVFUNC_1:def_16;
 u in EqClass (y,(CompF (P,G))) by A1, A17, Th5;
hence  (B_INF ((B_INF (a,(CompF (Q,G)))),(CompF (P,G)))) . y = FALSE by A18, BVFUNC_1:def_16; ::_thesis: verum
end;
thus  All ((All (a,P,G)),Q,G) = B_INF ((All (a,P,G)),(CompF (Q,G))) by BVFUNC_2:def_9
.= B_INF ((B_INF (a,(CompF (P,G)))),(CompF (Q,G))) by BVFUNC_2:def_9
.= B_INF ((B_INF (a,(CompF (Q,G)))),(CompF (P,G))) by A5, BVFUNC_1:def_16
.= B_INF ((All (a,Q,G)),(CompF (P,G))) by BVFUNC_2:def_9
.= All ((All (a,Q,G)),P,G) by BVFUNC_2:def_9 ; ::_thesis: verum
end;

theorem :: PARTIT_2:16
for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for P, Q being a_partition of Y st G is independent holds
Ex ((Ex (a,P,G)),Q,G) = Ex ((Ex (a,Q,G)),P,G)
proof
let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for P, Q being a_partition of Y st G is independent holds
Ex ((Ex (a,P,G)),Q,G) = Ex ((Ex (a,Q,G)),P,G)
let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y)
for P, Q being a_partition of Y st G is independent holds
Ex ((Ex (a,P,G)),Q,G) = Ex ((Ex (a,Q,G)),P,G)
let G be Subset of (PARTITIONS Y); ::_thesis: for P, Q being a_partition of Y st G is independent holds
Ex ((Ex (a,P,G)),Q,G) = Ex ((Ex (a,Q,G)),P,G)
let P, Q be a_partition of Y; ::_thesis: ( G is independent implies Ex ((Ex (a,P,G)),Q,G) = Ex ((Ex (a,Q,G)),P,G) )
assume A1: G is independent ; ::_thesis: Ex ((Ex (a,P,G)),Q,G) = Ex ((Ex (a,Q,G)),P,G)
thus  Ex ((Ex (a,P,G)),Q,G) = 'not' ('not' (Ex ((Ex (a,P,G)),Q,G)))
.= 'not' (All (('not' (Ex (a,P,G))),Q,G)) by BVFUNC_2:19
.= 'not' (All ((All (('not' a),P,G)),Q,G)) by BVFUNC_2:19
.= 'not' (All ((All (('not' a),Q,G)),P,G)) by A1, Th15
.= 'not' (All (('not' (Ex (a,Q,G))),P,G)) by BVFUNC_2:19
.= 'not' ('not' (Ex ((Ex (a,Q,G)),P,G))) by BVFUNC_2:19
.= Ex ((Ex (a,Q,G)),P,G) ; ::_thesis: verum
end;

theorem :: PARTIT_2:17
for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for P, Q being a_partition of Y st G is independent holds
Ex ((All (a,P,G)),Q,G) '<' All ((Ex (a,Q,G)),P,G)
proof
let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for P, Q being a_partition of Y st G is independent holds
Ex ((All (a,P,G)),Q,G) '<' All ((Ex (a,Q,G)),P,G)
let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y)
for P, Q being a_partition of Y st G is independent holds
Ex ((All (a,P,G)),Q,G) '<' All ((Ex (a,Q,G)),P,G)
let G be Subset of (PARTITIONS Y); ::_thesis: for P, Q being a_partition of Y st G is independent holds
Ex ((All (a,P,G)),Q,G) '<' All ((Ex (a,Q,G)),P,G)
let P, Q be a_partition of Y; ::_thesis: ( G is independent implies Ex ((All (a,P,G)),Q,G) '<' All ((Ex (a,Q,G)),P,G) )
assume A1: G is independent ; ::_thesis: Ex ((All (a,P,G)),Q,G) '<' All ((Ex (a,Q,G)),P,G)
set A = G \ {P};
set B = G \ {Q};
 ( G \ {P} c= G & G \ {Q} c= G ) by XBOOLE_1:36;
then A2: (ERl ('/\' (G \ {P}))) * (ERl ('/\' (G \ {Q}))) = (ERl ('/\' (G \ {Q}))) * (ERl ('/\' (G \ {P}))) by A1, Th14;
A3: CompF (P,G) = '/\' (G \ {P}) by BVFUNC_2:def_7;
A4: Ex ((All (a,P,G)),Q,G) = B_SUP ((All (a,P,G)),(CompF (Q,G))) by BVFUNC_2:def_10;
A5: CompF (Q,G) = '/\' (G \ {Q}) by BVFUNC_2:def_7;
let x be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (Ex ((All (a,P,G)),Q,G)) . x = TRUE or (All ((Ex (a,Q,G)),P,G)) . x = TRUE )
assume A6: (Ex ((All (a,P,G)),Q,G)) . x = TRUE ; ::_thesis: (All ((Ex (a,Q,G)),P,G)) . x = TRUE
A7: for z being Element of Y st z in EqClass (x,(CompF (P,G))) holds
(Ex (a,Q,G)) . z = TRUE
proof
let z be Element of Y; ::_thesis: ( z in EqClass (x,(CompF (P,G))) implies (Ex (a,Q,G)) . z = TRUE )
consider y being Element of Y such that
A8: y in EqClass (x,(CompF (Q,G))) and
A9: (All (a,P,G)) . y = TRUE by A6, A4, BVFUNC_1:def_17;
assume  z in EqClass (x,(CompF (P,G))) ; ::_thesis: (Ex (a,Q,G)) . z = TRUE
then  [z,x] in ERl ('/\' (G \ {P})) by A3, Th5;
then A10: [x,z] in ERl ('/\' (G \ {P})) by EQREL_1:6;
 [y,x] in ERl ('/\' (G \ {Q})) by A5, A8, Th5;
then  [y,z] in (ERl ('/\' (G \ {P}))) * (ERl ('/\' (G \ {Q}))) by A2, A10, RELAT_1:def_8;
then consider u being set  such that
A11: [y,u] in ERl ('/\' (G \ {P})) and
A12: [u,z] in ERl ('/\' (G \ {Q})) by RELAT_1:def_8;
 u in field (ERl ('/\' (G \ {Q}))) by A12, RELAT_1:15;
then reconsider u = u as Element of Y by ORDERS_1:12;
 [u,y] in ERl ('/\' (G \ {P})) by A11, EQREL_1:6;
then  ( All (a,P,G) = B_INF (a,(CompF (P,G))) & u in EqClass (y,(CompF (P,G))) ) by A3, Th5, BVFUNC_2:def_9;
then A13: a . u = TRUE by A9, BVFUNC_1:def_16;
 ( Ex (a,Q,G) = B_SUP (a,(CompF (Q,G))) & u in EqClass (z,(CompF (Q,G))) ) by A5, A12, Th5, BVFUNC_2:def_10;
hence  (Ex (a,Q,G)) . z = TRUE by A13, BVFUNC_1:def_17; ::_thesis: verum
end;
 All ((Ex (a,Q,G)),P,G) = B_INF ((Ex (a,Q,G)),(CompF (P,G))) by BVFUNC_2:def_9;
hence  (All ((Ex (a,Q,G)),P,G)) . x = TRUE by A7, BVFUNC_1:def_16; ::_thesis: verum
end;

begin


notation
let A, B be set ;
synonym  [#] (A,B) for [:A,B:];
end;

definition
let A, B be set ;
func {} (A,B) ->  Relation of A,B equals :: PARTIT_2:def 1
 {} ;
correctness
coherence
{} is Relation of A,B;
by RELSET_1:12;
:: original: [#]
redefine func [#] (A,B) ->  Relation of A,B;
correctness
coherence
[#] (A,B) is Relation of A,B;
proof
 [#] (A,B) c= [:A,B:] ;
hence  [#] (A,B) is Relation of A,B ; ::_thesis: verum
end;
end;

:: deftheorem  defines {} PARTIT_2:def_1_:_
 for A, B being set holds {} (A,B) = {} ;

registration
let A, B be set ;
cluster {} (A,B) ->  empty ;
coherence
 {} (A,B) is empty ;
end;

theorem :: PARTIT_2:18
for X being non empty set holds field (id X) = X
proof
let X be non empty set ; ::_thesis: field (id X) = X
 ( dom (id X) = X & rng (id X) = X ) ;
then  field (id X) = X \/ X by RELAT_1:def_6;
hence  field (id X) = X ; ::_thesis: verum
end;

theorem :: PARTIT_2:19
op1 = {[{},{}]}
proof
 {{}} = dom op1 by CARD_1:49, FUNCT_2:def_1;
then  {} in dom op1 by TARSKI:def_1;
then  [{},(op1 . {})] in op1 by FUNCT_1:def_2;
then A1: {[{},(op1 . {})]} c= op1 by ZFMISC_1:31;
 rng op1 = {(op1 . {})} by CARD_1:49, FUNCT_2:48;
then A2: op1 . {} = {} by CARD_1:49, ZFMISC_1:18;
 op1 c= [:{{}},{{}}:] by CARD_1:49;
then  op1 c= {[{},{}]} by ZFMISC_1:29;
hence  op1 = {[{},{}]} by A2, A1, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: PARTIT_2:20
for A, B being set holds field ({} (A,B)) = {} by RELAT_1:40;

theorem :: PARTIT_2:21
for X being non empty set
for R being Relation of X st R is_reflexive_in X holds
( R is reflexive & field R = X )
proof
let X be non empty set ; ::_thesis: for R being Relation of X st R is_reflexive_in X holds
( R is reflexive & field R = X )
let R be Relation of X; ::_thesis: ( R is_reflexive_in X implies ( R is reflexive & field R = X ) )
assume A1: R is_reflexive_in X ; ::_thesis: ( R is reflexive & field R = X )
then  X = field R by Th9;
hence  ( R is reflexive & field R = X ) by A1, RELAT_2:def_9; ::_thesis: verum
end;

theorem :: PARTIT_2:22
for X being non empty set
for R being Relation of X st R is_symmetric_in X holds
R is symmetric
proof
let X be non empty set ; ::_thesis: for R being Relation of X st R is_symmetric_in X holds
R is symmetric
let R be Relation of X; ::_thesis: ( R is_symmetric_in X implies R is symmetric )
assume A1: R is_symmetric_in X ; ::_thesis: R is symmetric
let x, y be set ; :: according to RELAT_2:def_3,RELAT_2:def_11 ::_thesis: ( not x in field R or not y in field R or not [x,y] in R or [y,x] in R )
 field R c= X \/ X by RELSET_1:8;
hence  ( not x in field R or not y in field R or not [x,y] in R or [y,x] in R ) by A1, RELAT_2:def_3; ::_thesis: verum
end;

theorem :: PARTIT_2:23
for X, S being non empty set
for R being Relation of X st R is symmetric holds
R is_symmetric_in S
proof
let X, S be non empty set ; ::_thesis: for R being Relation of X st R is symmetric holds
R is_symmetric_in S
let R be Relation of X; ::_thesis: ( R is symmetric implies R is_symmetric_in S )
assume  R is symmetric ; ::_thesis: R is_symmetric_in S
then A1: R is_symmetric_in field R by RELAT_2:def_11;
let x, y be set ; :: according to RELAT_2:def_3 ::_thesis: ( not x in S or not y in S or not [x,y] in R or [y,x] in R )
assume  ( x in S & y in S ) ; ::_thesis: ( not [x,y] in R or [y,x] in R )
assume A2: [x,y] in R ; ::_thesis: [y,x] in R
then  ( x in field R & y in field R ) by RELAT_1:15;
hence  [y,x] in R by A1, A2, RELAT_2:def_3; ::_thesis: verum
end;

theorem :: PARTIT_2:24
for X, S being non empty set
for R being Relation of X st R is antisymmetric holds
R is_antisymmetric_in S
proof
let X, S be non empty set ; ::_thesis: for R being Relation of X st R is antisymmetric holds
R is_antisymmetric_in S
let R be Relation of X; ::_thesis: ( R is antisymmetric implies R is_antisymmetric_in S )
assume  R is antisymmetric ; ::_thesis: R is_antisymmetric_in S
then A1: R is_antisymmetric_in field R by RELAT_2:def_12;
let x, y be set ; :: according to RELAT_2:def_4 ::_thesis: ( not x in S or not y in S or not [x,y] in R or not [y,x] in R or x = y )
assume  ( x in S & y in S ) ; ::_thesis: ( not [x,y] in R or not [y,x] in R or x = y )
assume A2: [x,y] in R ; ::_thesis: ( not [y,x] in R or x = y )
then  ( x in field R & y in field R ) by RELAT_1:15;
hence  ( not [y,x] in R or x = y ) by A1, A2, RELAT_2:def_4; ::_thesis: verum
end;

theorem :: PARTIT_2:25
for X being non empty set
for R being Relation of X st R is_antisymmetric_in X holds
R is antisymmetric
proof
let X be non empty set ; ::_thesis: for R being Relation of X st R is_antisymmetric_in X holds
R is antisymmetric
let R be Relation of X; ::_thesis: ( R is_antisymmetric_in X implies R is antisymmetric )
assume A1: R is_antisymmetric_in X ; ::_thesis: R is antisymmetric
let x, y be set ; :: according to RELAT_2:def_4,RELAT_2:def_12 ::_thesis: ( not x in field R or not y in field R or not [x,y] in R or not [y,x] in R or x = y )
 field R c= X \/ X by RELSET_1:8;
hence  ( not x in field R or not y in field R or not [x,y] in R or not [y,x] in R or x = y ) by A1, RELAT_2:def_4; ::_thesis: verum
end;

theorem :: PARTIT_2:26
for X, S being non empty set
for R being Relation of X st R is transitive holds
R is_transitive_in S
proof
let X, S be non empty set ; ::_thesis: for R being Relation of X st R is transitive holds
R is_transitive_in S
let R be Relation of X; ::_thesis: ( R is transitive implies R is_transitive_in S )
assume  R is transitive ; ::_thesis: R is_transitive_in S
then A1: R is_transitive_in field R by RELAT_2:def_16;
let x, y, z be set ; :: according to RELAT_2:def_8 ::_thesis: ( not x in S or not y in S or not z in S or not [x,y] in R or not [y,z] in R or [x,z] in R )
assume  ( x in S & y in S & z in S ) ; ::_thesis: ( not [x,y] in R or not [y,z] in R or [x,z] in R )
assume A2: [x,y] in R ; ::_thesis: ( not [y,z] in R or [x,z] in R )
then A3: x in field R by RELAT_1:15;
assume A4: [y,z] in R ; ::_thesis: [x,z] in R
then  ( y in field R & z in field R ) by RELAT_1:15;
hence  [x,z] in R by A1, A2, A4, A3, RELAT_2:def_8; ::_thesis: verum
end;

theorem :: PARTIT_2:27
for X being non empty set
for R being Relation of X st R is_transitive_in X holds
R is transitive
proof
let X be non empty set ; ::_thesis: for R being Relation of X st R is_transitive_in X holds
R is transitive
let R be Relation of X; ::_thesis: ( R is_transitive_in X implies R is transitive )
assume A1: R is_transitive_in X ; ::_thesis: R is transitive
let x, y, z be set ; :: according to RELAT_2:def_8,RELAT_2:def_16 ::_thesis: ( not x in field R or not y in field R or not z in field R or not [x,y] in R or not [y,z] in R or [x,z] in R )
 field R c= X \/ X by RELSET_1:8;
hence  ( not x in field R or not y in field R or not z in field R or not [x,y] in R or not [y,z] in R or [x,z] in R ) by A1, RELAT_2:def_8; ::_thesis: verum
end;

theorem :: PARTIT_2:28
for X, S being non empty set
for R being Relation of X st R is asymmetric holds
R is_asymmetric_in S
proof
let X, S be non empty set ; ::_thesis: for R being Relation of X st R is asymmetric holds
R is_asymmetric_in S
let R be Relation of X; ::_thesis: ( R is asymmetric implies R is_asymmetric_in S )
assume  R is asymmetric ; ::_thesis: R is_asymmetric_in S
then A1: R is_asymmetric_in field R by RELAT_2:def_13;
let x, y be set ; :: according to RELAT_2:def_5 ::_thesis: ( not x in S or not y in S or not [x,y] in R or not [y,x] in R )
assume  ( x in S & y in S ) ; ::_thesis: ( not [x,y] in R or not [y,x] in R )
assume A2: [x,y] in R ; ::_thesis: not [y,x] in R
then  ( x in field R & y in field R ) by RELAT_1:15;
hence  not [y,x] in R by A1, A2, RELAT_2:def_5; ::_thesis: verum
end;

theorem :: PARTIT_2:29
for X being non empty set
for R being Relation of X st R is_asymmetric_in X holds
R is asymmetric
proof
let X be non empty set ; ::_thesis: for R being Relation of X st R is_asymmetric_in X holds
R is asymmetric
let R be Relation of X; ::_thesis: ( R is_asymmetric_in X implies R is asymmetric )
assume A1: R is_asymmetric_in X ; ::_thesis: R is asymmetric
let x, y be set ; :: according to RELAT_2:def_5,RELAT_2:def_13 ::_thesis: ( not x in field R or not y in field R or not [x,y] in R or not [y,x] in R )
 field R c= X \/ X by RELSET_1:8;
hence  ( not x in field R or not y in field R or not [x,y] in R or not [y,x] in R ) by A1, RELAT_2:def_5; ::_thesis: verum
end;

theorem :: PARTIT_2:30
for X, S being non empty set
for R being Relation of X st R is irreflexive & field R c= S holds
R is_irreflexive_in S
proof
let X, S be non empty set ; ::_thesis: for R being Relation of X st R is irreflexive & field R c= S holds
R is_irreflexive_in S
let R be Relation of X; ::_thesis: ( R is irreflexive & field R c= S implies R is_irreflexive_in S )
assume that
A1: R is irreflexive and
A2: field R c= S ; ::_thesis: R is_irreflexive_in S
let x be set ; :: according to RELAT_2:def_2 ::_thesis: ( not x in S or not [x,x] in R )
 S = (field R) \/ (S \ (field R)) by A2, XBOOLE_1:45;
then A3: ( not x in S or x in field R or x in S \ (field R) ) by XBOOLE_0:def_3;
A4: ( x in S \ (field R) implies not [x,x] in R )
proof
assume  x in S \ (field R) ; ::_thesis: not [x,x] in R
then  x in S \ ((dom R) \/ (rng R)) by RELAT_1:def_6;
then  x in (S \ (dom R)) /\ (S \ (rng R)) by XBOOLE_1:53;
then  x in S \ (rng R) by XBOOLE_0:def_4;
then  not x in rng R by XBOOLE_0:def_5;
hence  not [x,x] in R by XTUPLE_0:def_13; ::_thesis: verum
end;
 R is_irreflexive_in field R by A1, RELAT_2:def_10;
hence  ( not x in S or not [x,x] in R ) by A3, A4, RELAT_2:def_2; ::_thesis: verum
end;

theorem :: PARTIT_2:31
for X being non empty set
for R being Relation of X st R is_irreflexive_in X holds
R is irreflexive
proof
let X be non empty set ; ::_thesis: for R being Relation of X st R is_irreflexive_in X holds
R is irreflexive
let R be Relation of X; ::_thesis: ( R is_irreflexive_in X implies R is irreflexive )
A1: field R c= X \/ X by RELSET_1:8;
assume  R is_irreflexive_in X ; ::_thesis: R is irreflexive
then  for x being set st x in field R holds
not [x,x] in R by A1, RELAT_2:def_2;
then  R is_irreflexive_in field R by RELAT_2:def_2;
hence  R is irreflexive by RELAT_2:def_10; ::_thesis: verum
end;

registration
cluster empty Relation-like  ->  irreflexive asymmetric transitive for set ;
coherence
 for b1 being Relation st b1 is empty holds
( b1 is irreflexive & b1 is asymmetric & b1 is transitive )
proof
let R be Relation; ::_thesis: ( R is empty implies ( R is irreflexive & R is asymmetric & R is transitive ) )
assume A1: R is empty ; ::_thesis: ( R is irreflexive & R is asymmetric & R is transitive )
hence  for x being set st x in field R holds
not [x,x] in R ; :: according to RELAT_2:def_2,RELAT_2:def_10 ::_thesis: ( R is asymmetric & R is transitive )
thus  for x, y being set st x in field R & y in field R & [x,y] in R holds
not [y,x] in R by A1; :: according to RELAT_2:def_5,RELAT_2:def_13 ::_thesis: R is transitive
thus  for x, y, z being set st x in field R & y in field R & z in field R & [x,y] in R & [y,z] in R holds
[x,z] in R by A1; :: according to RELAT_2:def_8,RELAT_2:def_16 ::_thesis: verum
end;
end;

definition
let f be Function;
attrf is involutive  means :Def2: :: PARTIT_2:def 2
 for x being set st x in dom f holds
f . (f . x) = x;
end;

:: deftheorem Def2 defines involutive PARTIT_2:def_2_:_
 for f being Function holds
( f is involutive iff for x being set st x in dom f holds
f . (f . x) = x );

definition
let X be non empty set ;
let f be UnOp of X;
:: original: involutive
redefine attrf is involutive  means :: PARTIT_2:def 3
 for x being Element of X holds f . (f . x) = x;
compatibility
 ( f is involutive iff for x being Element of X holds f . (f . x) = x )
proof
 dom f = X by PARTFUN1:def_2;
hence  ( f is involutive implies for x being Element of X holds f . (f . x) = x ) by Def2; ::_thesis: ( ( for x being Element of X holds f . (f . x) = x ) implies f is involutive )
assume A1: for x being Element of X holds f . (f . x) = x ; ::_thesis: f is involutive
let x be set ; :: according to PARTIT_2:def_2 ::_thesis: ( x in dom f implies f . (f . x) = x )
assume  x in dom f ; ::_thesis: f . (f . x) = x
hence  f . (f . x) = x by A1; ::_thesis: verum
end;
end;

:: deftheorem  defines involutive PARTIT_2:def_3_:_
 for X being non empty set
for f being UnOp of X holds
( f is involutive iff for x being Element of X holds f . (f . x) = x );

registration
cluster op1  ->  involutive for Function;
coherence
 for b1 being Function st b1 = op1 holds
b1 is involutive
proof
 op1 is ()
proof
let a be Element of 1; :: according to PARTIT_2:def_3 ::_thesis: op1 . (op1 . a) = a
 a = {} by CARD_1:49, TARSKI:def_1;
hence  op1 . (op1 . a) = a by CARD_1:49, FUNCT_2:50; ::_thesis: verum
end;
hence  for b1 being Function st b1 = op1 holds
b1 is involutive ; ::_thesis: verum
end;
end;

registration
let X be set ;
cluster id X ->  involutive ;
coherence
 id X is involutive
proof
set f = id X;
let a be set ; :: according to PARTIT_2:def_2 ::_thesis: ( a in dom (id X) implies (id X) . ((id X) . a) = a )
assume  a in dom (id X) ; ::_thesis: (id X) . ((id X) . a) = a
then  a in X ;
then  (id X) . a = a by FUNCT_1:17;
hence  (id X) . ((id X) . a) = a ; ::_thesis: verum
end;
end;