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

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)

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

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 )

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

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

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

for Y being non empty set
for a, b being Element of Funcs 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

for Y being non empty set
for a being Element of Funcs 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

for Y being non empty set
for a being Element of Funcs 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

for Y being non empty set
for a being Element of Funcs 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

for Y being non empty set
for a being Element of Funcs 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

for Y being non empty set
for a being Element of Funcs 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

for Y being non empty set
for a being Element of Funcs 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

for Y being non empty set
for a being Element of Funcs 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

for Y being non empty set
for a being Element of Funcs 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

for Y being non empty set
for a being Element of Funcs 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

for Y being non empty set
for a being Element of Funcs 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

for Y being non empty set
for a being Element of Funcs 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

for Y being non empty set
for a being Element of Funcs 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

for Y being non empty set
for a being Element of Funcs 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

for Y being non empty set
for a being Element of Funcs 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

for Y being non empty set
for a being Element of Funcs 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

for Y being non empty set
for a being Element of Funcs 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

for Y being non empty set
for a being Element of Funcs 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