:: PARTIT_2 semantic presentation
:: deftheorem Def1 defines c= PARTIT_2:def 1 :
theorem Th1: :: PARTIT_2:1
theorem Th2: :: PARTIT_2:2
theorem Th3: :: PARTIT_2:3
theorem Th4: :: PARTIT_2:4
theorem Th5: :: PARTIT_2:5
theorem Th6: :: PARTIT_2:6
theorem Th7: :: PARTIT_2:7
theorem Th8: :: PARTIT_2:8
theorem Th9: :: PARTIT_2:9
theorem Th10: :: PARTIT_2:10
theorem Th11: :: PARTIT_2:11
theorem Th12: :: PARTIT_2:12
canceled;
theorem Th13: :: PARTIT_2:13
theorem Th14: :: PARTIT_2:14
canceled;
theorem Th15: :: PARTIT_2:15
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))
theorem Th16: :: PARTIT_2:16
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
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
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