:: PARTIT_2 semantic presentation

definition
let c1, c2 be set ;
let c3, c4 be Relation of c1,c2;
redefine pred c= as c3 c= c4 means :: PARTIT_2:def 1
for b1 being Element of a1
for b2 being Element of a2 st [b1,b2] in a3 holds
[b1,b2] in a4;
compatibility
( c3 c= c4 iff for b1 being Element of c1
for b2 being Element of c2 st [b1,b2] in c3 holds
[b1,b2] in c4 )
proof end;
end;

:: deftheorem Def1 defines c= PARTIT_2:def 1 :
for b1, b2 being set
for b3, b4 being Relation of b1,b2 holds
( b3 c= b4 iff for b5 being Element of b1
for b6 being Element of b2 st [b5,b6] in b3 holds
[b5,b6] in b4 );

definition
let c1 be non empty set ;
let c2 be non empty Subset of (PARTITIONS c1);
redefine mode Element as Element of c2 -> a_partition of a1;
coherence
for b1 being Element of c2 holds b1 is a_partition of c1
proof end;
end;

theorem Th1: :: PARTIT_2:1
for b1 being non empty set holds '/\' ({} (PARTITIONS b1)) = %O b1
proof end;

theorem Th2: :: PARTIT_2:2
for b1 being non empty set
for b2, b3 being Equivalence_Relation of b1 holds b2 \/ b3 c= b2 * b3
proof end;

theorem Th3: :: PARTIT_2:3
for b1 being non empty set
for b2 being Relation of b1 holds b2 c= nabla b1
proof end;

theorem Th4: :: PARTIT_2:4
for b1 being non empty set
for b2 being Equivalence_Relation of b1 holds
( (nabla b1) * b2 = nabla b1 & b2 * (nabla b1) = nabla b1 )
proof end;

theorem Th5: :: PARTIT_2:5
for b1 being non empty set
for b2 being a_partition of b1
for b3, b4 being Element of b1 holds
( [b3,b4] in ERl b2 iff b3 in EqClass b4,b2 )
proof end;

theorem Th6: :: PARTIT_2:6
for b1 being non empty set
for b2, b3, b4 being a_partition of b1 st ERl b4 = (ERl b2) * (ERl b3) holds
for b5, b6 being Element of b1 holds
( b5 in EqClass b6,b4 iff ex b7 being Element of b1 st
( b5 in EqClass b7,b2 & b7 in EqClass b6,b3 ) )
proof end;

theorem Th7: :: PARTIT_2:7
for b1, b2 being Relation
for b3 being set st b1 is_reflexive_in b3 & b2 is_reflexive_in b3 holds
b1 * b2 is_reflexive_in b3
proof end;

theorem Th8: :: PARTIT_2:8
for b1 being Relation
for b2 being set st b1 is_reflexive_in b2 holds
b2 c= field b1
proof end;

theorem Th9: :: PARTIT_2:9
for b1 being set
for b2 being Relation of b1 st b2 is_reflexive_in b1 holds
b1 = field b2
proof end;

theorem Th10: :: PARTIT_2:10
for b1 being non empty set
for b2, b3 being Equivalence_Relation of b1 st b2 * b3 = b3 * b2 holds
b2 * b3 is Equivalence_Relation of b1
proof end;

theorem Th11: :: PARTIT_2:11
for b1 being non empty set
for b2, b3 being Element of Funcs b1,BOOLEAN st b2 '<' b3 holds
'not' b3 '<' 'not' b2
proof end;

theorem Th12: :: PARTIT_2:12
canceled;

theorem Th13: :: PARTIT_2:13
for b1 being non empty set
for b2, b3 being Element of Funcs b1,BOOLEAN
for b4 being Subset of (PARTITIONS b1)
for b5 being a_partition of b1 st b2 '<' b3 holds
All b2,b5,b4 '<' All b3,b5,b4
proof end;

theorem Th14: :: PARTIT_2:14
canceled;

theorem Th15: :: PARTIT_2:15
for b1 being non empty set
for b2, b3 being Element of Funcs b1,BOOLEAN
for b4 being Subset of (PARTITIONS b1)
for b5 being a_partition of b1 st b2 '<' b3 holds
Ex b2,b5,b4 '<' Ex b3,b5,b4
proof end;

Lemma10: for b1 being non empty set
for b2 being Subset of (PARTITIONS b1) st b2 is independent holds
for b3, b4 being Subset of (PARTITIONS b1) st b3 c= b2 & b4 c= b2 holds
(ERl ('/\' b3)) * (ERl ('/\' b4)) c= (ERl ('/\' b4)) * (ERl ('/\' b3))
proof end;

theorem Th16: :: PARTIT_2:16
for b1 being non empty set
for b2 being Subset of (PARTITIONS b1) st b2 is independent holds
for b3, b4 being Subset of (PARTITIONS b1) st b3 c= b2 & b4 c= b2 holds
(ERl ('/\' b3)) * (ERl ('/\' b4)) = (ERl ('/\' b4)) * (ERl ('/\' b3))
proof end;

theorem Th17: :: PARTIT_2:17
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN
for b3 being Subset of (PARTITIONS b1)
for b4, b5 being a_partition of b1 st b3 is independent holds
All (All b2,b4,b3),b5,b3 = All (All b2,b5,b3),b4,b3
proof end;

theorem Th18: :: PARTIT_2:18
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN
for b3 being Subset of (PARTITIONS b1)
for b4, b5 being a_partition of b1 st b3 is independent holds
Ex (Ex b2,b4,b3),b5,b3 = Ex (Ex b2,b5,b3),b4,b3
proof end;

theorem Th19: :: PARTIT_2:19
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN
for b3 being Subset of (PARTITIONS b1)
for b4, b5 being a_partition of b1 st b3 is independent holds
Ex (All b2,b4,b3),b5,b3 '<' All (Ex b2,b5,b3),b4,b3
proof end;