:: Predicate Calculus for Boolean Valued Functions, III
:: by Shunichi Kobayashi and Yatsuka Nakamura
::
:: Received July 14, 1999
:: Copyright (c) 1999-2021 Association of Mizar Users

theorem Th1: :: BVFUNC11:1

for Y being non empty set
for z being Element of Y
for PA, PB being a_partition of Y st PA '<' PB holds
EqClass (z,PA) c= EqClass (z,PB)

proof end;

theorem :: BVFUNC11:2

for Y being non empty set
for z being Element of Y
for PA, PB being a_partition of Y holds EqClass (z,PA) c= EqClass (z,(PA '\/' PB)) by Th1, PARTIT1:16;

theorem :: BVFUNC11:3

for Y being non empty set
for z being Element of Y
for PA, PB being a_partition of Y holds EqClass (z,(PA '/\' PB)) c= EqClass (z,PA) by Th1, PARTIT1:15;

theorem :: BVFUNC11:4

for Y being non empty set
for z being Element of Y
for PA being a_partition of Y holds
( EqClass (z,PA) c= EqClass (z,(%O Y)) & EqClass (z,(%I Y)) c= EqClass (z,PA) ) by Th1, PARTIT1:32;

theorem :: BVFUNC11:5

for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent & G = {A,B} & A <> B holds
for a, b being set st a in A & b in B holds
a meets b

proof end;

theorem :: BVFUNC11:6

for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent & G = {A,B} & A <> B holds
'/\' G = A '/\' B

proof end;

theorem :: BVFUNC11:7

for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G = {A,B} & A <> B holds
CompF (A,G) = B

proof end;

theorem Th8: :: BVFUNC11:8

for Y being non empty set
for a, b being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A being a_partition of Y st a '<' b holds
All (a,A,G) '<' Ex (b,A,G)

proof end;

theorem Th9: :: BVFUNC11:9

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
All ((All (a,A,G)),B,G) '<' Ex ((All (a,B,G)),A,G)

proof end;

theorem :: BVFUNC11:10

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y holds All ((All (a,A,G)),B,G) '<' Ex ((Ex (a,B,G)),A,G)

proof end;

theorem :: BVFUNC11:11

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
All ((All (a,A,G)),B,G) '<' All ((Ex (a,B,G)),A,G)

proof end;

theorem :: BVFUNC11:12

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y holds All ((Ex (a,A,G)),B,G) '<' Ex ((Ex (a,B,G)),A,G)

proof end;

theorem Th13: :: BVFUNC11:13

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y holds 'not' (Ex ((All (a,A,G)),B,G)) '<' Ex ((Ex (('not' a),B,G)),A,G)

proof end;

theorem Th14: :: BVFUNC11:14

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
Ex (('not' (All (a,A,G))),B,G) '<' Ex ((Ex (('not' a),B,G)),A,G)

proof end;

theorem Th15: :: BVFUNC11:15

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
'not' (All ((All (a,A,G)),B,G)) = Ex (('not' (All (a,B,G))),A,G)

proof end;

theorem :: BVFUNC11:16

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
All (('not' (All (a,A,G))),B,G) '<' Ex ((Ex (('not' a),B,G)),A,G)

proof end;

theorem :: BVFUNC11:17

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
'not' (All ((All (a,A,G)),B,G)) = Ex ((Ex (('not' a),B,G)),A,G)

proof end;

theorem :: BVFUNC11:18

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
'not' (All ((All (a,A,G)),B,G)) '<' Ex ((Ex (('not' a),A,G)),B,G)

proof end;

:: from BVFUNC12

theorem Th19: :: BVFUNC11:19

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y holds 'not' (All ((Ex (a,A,G)),B,G)) = Ex ((All (('not' a),A,G)),B,G)

proof end;

theorem Th20: :: BVFUNC11:20

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y holds 'not' (Ex ((All (a,A,G)),B,G)) = All ((Ex (('not' a),A,G)),B,G)

proof end;

theorem Th21: :: BVFUNC11:21

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y holds 'not' (All ((All (a,A,G)),B,G)) = Ex ((Ex (('not' a),A,G)),B,G)

proof end;

theorem :: BVFUNC11:22

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
Ex ((All (a,A,G)),B,G) '<' Ex ((Ex (a,B,G)),A,G)

proof end;

theorem :: BVFUNC11:23

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y holds All ((All (a,A,G)),B,G) '<' All ((Ex (a,A,G)),B,G)

proof end;

theorem :: BVFUNC11:24

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y holds All ((All (a,A,G)),B,G) '<' Ex ((Ex (a,A,G)),B,G)

proof end;

theorem :: BVFUNC11:25

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y holds Ex ((All (a,A,G)),B,G) '<' Ex ((Ex (a,A,G)),B,G)

proof end;

:: BVFUNC13

theorem Th26: :: BVFUNC11:26

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
All (('not' (All (a,A,G))),B,G) '<' 'not' (All ((All (a,B,G)),A,G))

proof end;

theorem Th27: :: BVFUNC11:27

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y holds All ((All (('not' a),A,G)),B,G) '<' 'not' (All ((All (a,B,G)),A,G))

proof end;

theorem Th28: :: BVFUNC11:28

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y holds All (('not' (Ex (a,A,G))),B,G) '<' 'not' (All ((All (a,B,G)),A,G))

proof end;

theorem Th29: :: BVFUNC11:29

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
All ((Ex (('not' a),A,G)),B,G) '<' 'not' (All ((All (a,B,G)),A,G))

proof end;

theorem :: BVFUNC11:30

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
Ex ((All (('not' a),A,G)),B,G) '<' 'not' (All ((All (a,B,G)),A,G))

proof end;

theorem Th31: :: BVFUNC11:31

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
Ex (('not' (Ex (a,A,G))),B,G) '<' 'not' (All ((All (a,B,G)),A,G))

proof end;

theorem :: BVFUNC11:32

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
'not' (All ((Ex (a,A,G)),B,G)) '<' 'not' (Ex ((All (a,B,G)),A,G)) by PARTIT_2:11, PARTIT_2:17;

theorem Th33: :: BVFUNC11:33

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
'not' (Ex ((Ex (a,A,G)),B,G)) '<' 'not' (Ex ((All (a,B,G)),A,G))

proof end;

theorem Th34: :: BVFUNC11:34

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y holds 'not' (Ex ((Ex (a,A,G)),B,G)) '<' 'not' (All ((Ex (a,B,G)),A,G))

proof end;

theorem :: BVFUNC11:35

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
'not' (Ex ((All (a,A,G)),B,G)) '<' 'not' (All ((All (a,B,G)),A,G))

proof end;

theorem :: BVFUNC11:36

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
'not' (All ((Ex (a,A,G)),B,G)) '<' 'not' (All ((All (a,B,G)),A,G))

proof end;

theorem :: BVFUNC11:37

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y holds 'not' (Ex ((Ex (a,A,G)),B,G)) '<' 'not' (All ((All (a,B,G)),A,G))

proof end;

theorem Th38: :: BVFUNC11:38

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
'not' (Ex ((All (a,A,G)),B,G)) '<' Ex (('not' (All (a,B,G))),A,G)

proof end;

theorem Th39: :: BVFUNC11:39

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
'not' (All ((Ex (a,A,G)),B,G)) '<' Ex (('not' (All (a,B,G))),A,G)

proof end;

theorem Th40: :: BVFUNC11:40

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y holds 'not' (Ex ((Ex (a,A,G)),B,G)) '<' Ex (('not' (All (a,B,G))),A,G)

proof end;

theorem Th41: :: BVFUNC11:41

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
'not' (All ((Ex (a,A,G)),B,G)) '<' All (('not' (All (a,B,G))),A,G)

proof end;

theorem Th42: :: BVFUNC11:42

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
'not' (Ex ((Ex (a,A,G)),B,G)) '<' All (('not' (All (a,B,G))),A,G)

proof end;

theorem Th43: :: BVFUNC11:43

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y holds 'not' (Ex ((Ex (a,A,G)),B,G)) '<' Ex (('not' (Ex (a,B,G))),A,G)

proof end;

theorem Th44: :: BVFUNC11:44

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
'not' (Ex ((Ex (a,A,G)),B,G)) = All (('not' (Ex (a,B,G))),A,G)

proof end;

theorem Th45: :: BVFUNC11:45

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
'not' (All ((Ex (a,A,G)),B,G)) '<' Ex ((Ex (('not' a),B,G)),A,G)

proof end;

theorem Th46: :: BVFUNC11:46

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y holds 'not' (Ex ((Ex (a,A,G)),B,G)) '<' Ex ((Ex (('not' a),B,G)),A,G)

proof end;

theorem Th47: :: BVFUNC11:47

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
'not' (All ((Ex (a,A,G)),B,G)) '<' All ((Ex (('not' a),B,G)),A,G)

proof end;

theorem Th48: :: BVFUNC11:48

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
'not' (Ex ((Ex (a,A,G)),B,G)) '<' All ((Ex (('not' a),B,G)),A,G)

proof end;

theorem Th49: :: BVFUNC11:49

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y holds 'not' (Ex ((Ex (a,A,G)),B,G)) '<' Ex ((All (('not' a),B,G)),A,G)

proof end;

theorem Th50: :: BVFUNC11:50

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
'not' (Ex ((Ex (a,A,G)),B,G)) = All ((All (('not' a),B,G)),A,G)

proof end;

theorem :: BVFUNC11:51

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
Ex (('not' (Ex (a,A,G))),B,G) '<' 'not' (Ex ((All (a,B,G)),A,G))

proof end;

theorem :: BVFUNC11:52

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y holds All (('not' (Ex (a,A,G))),B,G) '<' 'not' (Ex ((All (a,B,G)),A,G))

proof end;

theorem :: BVFUNC11:53

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y holds All (('not' (Ex (a,A,G))),B,G) '<' 'not' (All ((Ex (a,B,G)),A,G))

proof end;

theorem :: BVFUNC11:54

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
All (('not' (Ex (a,A,G))),B,G) = 'not' (Ex ((Ex (a,B,G)),A,G))

proof end;

theorem :: BVFUNC11:55

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
Ex (('not' (All (a,A,G))),B,G) = Ex (('not' (All (a,B,G))),A,G)

proof end;

theorem :: BVFUNC11:56

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
All (('not' (All (a,A,G))),B,G) '<' Ex (('not' (All (a,B,G))),A,G)

proof end;

theorem :: BVFUNC11:57

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
Ex (('not' (Ex (a,A,G))),B,G) '<' Ex (('not' (All (a,B,G))),A,G)

proof end;

theorem :: BVFUNC11:58

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y holds All (('not' (Ex (a,A,G))),B,G) '<' Ex (('not' (All (a,B,G))),A,G)

proof end;

theorem :: BVFUNC11:59

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
Ex (('not' (Ex (a,A,G))),B,G) '<' All (('not' (All (a,B,G))),A,G)

proof end;

theorem :: BVFUNC11:60

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
All (('not' (Ex (a,A,G))),B,G) '<' All (('not' (All (a,B,G))),A,G)

proof end;

theorem :: BVFUNC11:61

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y holds All (('not' (Ex (a,A,G))),B,G) '<' Ex (('not' (Ex (a,B,G))),A,G)

proof end;

theorem :: BVFUNC11:62

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
All (('not' (Ex (a,A,G))),B,G) = All (('not' (Ex (a,B,G))),A,G)

proof end;

theorem :: BVFUNC11:63

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
Ex (('not' (Ex (a,A,G))),B,G) '<' Ex ((Ex (('not' a),B,G)),A,G)

proof end;

theorem :: BVFUNC11:64

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y holds All (('not' (Ex (a,A,G))),B,G) '<' Ex ((Ex (('not' a),B,G)),A,G)

proof end;

theorem :: BVFUNC11:65

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
Ex (('not' (Ex (a,A,G))),B,G) '<' All ((Ex (('not' a),B,G)),A,G)

proof end;

theorem :: BVFUNC11:66

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
All (('not' (Ex (a,A,G))),B,G) '<' All ((Ex (('not' a),B,G)),A,G)

proof end;

theorem :: BVFUNC11:67

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y holds All (('not' (Ex (a,A,G))),B,G) '<' Ex ((All (('not' a),B,G)),A,G)

proof end;

theorem :: BVFUNC11:68

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
All (('not' (Ex (a,A,G))),B,G) = All ((All (('not' a),B,G)),A,G)

proof end;

theorem :: BVFUNC11:69

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
Ex ((All (('not' a),A,G)),B,G) '<' 'not' (Ex ((All (a,B,G)),A,G))

proof end;

theorem :: BVFUNC11:70

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
All ((All (('not' a),A,G)),B,G) '<' 'not' (Ex ((All (a,B,G)),A,G))

proof end;

theorem :: BVFUNC11:71

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y holds All ((All (('not' a),A,G)),B,G) '<' 'not' (All ((Ex (a,B,G)),A,G))

proof end;

theorem :: BVFUNC11:72

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
All ((All (('not' a),A,G)),B,G) '<' 'not' (Ex ((Ex (a,B,G)),A,G))

proof end;

theorem :: BVFUNC11:73

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
Ex ((Ex (('not' a),A,G)),B,G) '<' Ex (('not' (All (a,B,G))),A,G)

proof end;

theorem :: BVFUNC11:74

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
All ((Ex (('not' a),A,G)),B,G) '<' Ex (('not' (All (a,B,G))),A,G)

proof end;

theorem :: BVFUNC11:75

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
Ex ((All (('not' a),A,G)),B,G) '<' Ex (('not' (All (a,B,G))),A,G)

proof end;

theorem :: BVFUNC11:76

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y holds All ((All (('not' a),A,G)),B,G) '<' Ex (('not' (All (a,B,G))),A,G)

proof end;

theorem :: BVFUNC11:77

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
Ex ((All (('not' a),A,G)),B,G) '<' All (('not' (All (a,B,G))),A,G)

proof end;

theorem :: BVFUNC11:78

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
All ((All (('not' a),A,G)),B,G) '<' All (('not' (All (a,B,G))),A,G)

proof end;

theorem :: BVFUNC11:79

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y holds All ((All (('not' a),A,G)),B,G) '<' Ex (('not' (Ex (a,B,G))),A,G)

proof end;

theorem :: BVFUNC11:80

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
All ((All (('not' a),A,G)),B,G) = All (('not' (Ex (a,B,G))),A,G)

proof end;

theorem :: BVFUNC11:81

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y holds All ((Ex (('not' a),A,G)),B,G) '<' Ex ((Ex (('not' a),B,G)),A,G)

proof end;

theorem :: BVFUNC11:82

for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
Ex ((All (('not' a),A,G)),B,G) '<' Ex ((Ex (('not' a),B,G)),A,G)

proof end;