:: BVFUNC11 semantic presentation
begin
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
let Y be non empty set ; ::_thesis: 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)
let z be Element of Y; ::_thesis: for PA, PB being a_partition of Y st PA '<' PB holds
EqClass (z,PA) c= EqClass (z,PB)
let PA, PB be a_partition of Y; ::_thesis: ( PA '<' PB implies EqClass (z,PA) c= EqClass (z,PB) )
assume PA '<' PB ; ::_thesis: EqClass (z,PA) c= EqClass (z,PB)
then A1: ex b being set st
( b in PB & EqClass (z,PA) c= b ) by SETFAM_1:def_2;
z in EqClass (z,PA) by EQREL_1:def_6;
hence EqClass (z,PA) c= EqClass (z,PB) by A1, EQREL_1:def_6; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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
let G be Subset of (PARTITIONS Y); ::_thesis: 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
let A, B be a_partition of Y; ::_thesis: ( G is independent & G = {A,B} & A <> B implies for a, b being set st a in A & b in B holds
a meets b )
assume that
A1: G is independent and
A2: G = {A,B} and
A3: A <> B ; ::_thesis: for a, b being set st a in A & b in B holds
a meets b
let a, b be set ; ::_thesis: ( a in A & b in B implies a meets b )
assume that
A4: a in A and
A5: b in B ; ::_thesis: a meets b
set h2 = (A,B) --> (a,b);
A6: for d being set st d in G holds
((A,B) --> (a,b)) . d in d
proof
let d be set ; ::_thesis: ( d in G implies ((A,B) --> (a,b)) . d in d )
assume d in G ; ::_thesis: ((A,B) --> (a,b)) . d in d
then ( d = A or d = B ) by A2, TARSKI:def_2;
hence ((A,B) --> (a,b)) . d in d by A3, A4, A5, FUNCT_4:63; ::_thesis: verum
end;
{a,b} c= bool Y
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {a,b} or x in bool Y )
assume x in {a,b} ; ::_thesis: x in bool Y
then ( x = a or x = b ) by TARSKI:def_2;
hence x in bool Y by A4, A5; ::_thesis: verum
end;
then reconsider SS = {a,b} as Subset-Family of Y ;
A7: dom ((A,B) --> (a,b)) = {A,B} by FUNCT_4:62;
rng ((A,B) --> (a,b)) = SS by A3, FUNCT_4:64;
then Intersect SS <> {} by A1, A2, A7, A6, BVFUNC_2:def_5;
hence a /\ b <> {} by A4, A5, MSSUBFAM:10; :: according to XBOOLE_0:def_7 ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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
let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y st G is independent & G = {A,B} & A <> B holds
'/\' G = A '/\' B
let A, B be a_partition of Y; ::_thesis: ( G is independent & G = {A,B} & A <> B implies '/\' G = A '/\' B )
assume that
A1: G is independent and
A2: G = {A,B} and
A3: A <> B ; ::_thesis: '/\' G = A '/\' B
A4: '/\' G c= A '/\' B
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in '/\' G or x in A '/\' B )
assume x in '/\' G ; ::_thesis: x in A '/\' B
then consider h being Function, F being Subset-Family of Y such that
A5: dom h = G and
A6: rng h = F and
A7: for d being set st d in G holds
h . d in d and
A8: x = Intersect F and
A9: x <> {} by BVFUNC_2:def_1;
A10: not x in {{}} by A9, TARSKI:def_1;
A11: A in G by A2, TARSKI:def_2;
then A12: h . A in rng h by A5, FUNCT_1:def_3;
then A13: Intersect F = meet (rng h) by A6, SETFAM_1:def_9;
A14: (h . A) /\ (h . B) c= x
proof
A15: rng h = {(h . A),(h . B)}
proof
thus rng h c= {(h . A),(h . B)} :: according to XBOOLE_0:def_10 ::_thesis: {(h . A),(h . B)} c= rng h
proof
let m be set ; :: according to TARSKI:def_3 ::_thesis: ( not m in rng h or m in {(h . A),(h . B)} )
assume m in rng h ; ::_thesis: m in {(h . A),(h . B)}
then consider w being set such that
A16: w in dom h and
A17: m = h . w by FUNCT_1:def_3;
( w = A or w = B ) by A2, A5, A16, TARSKI:def_2;
hence m in {(h . A),(h . B)} by A17, TARSKI:def_2; ::_thesis: verum
end;
let m be set ; :: according to TARSKI:def_3 ::_thesis: ( not m in {(h . A),(h . B)} or m in rng h )
assume m in {(h . A),(h . B)} ; ::_thesis: m in rng h
then A18: ( m = h . A or m = h . B ) by TARSKI:def_2;
A19: B in dom h by A2, A5, TARSKI:def_2;
A in dom h by A2, A5, TARSKI:def_2;
hence m in rng h by A18, A19, FUNCT_1:def_3; ::_thesis: verum
end;
let m be set ; :: according to TARSKI:def_3 ::_thesis: ( not m in (h . A) /\ (h . B) or m in x )
assume A20: m in (h . A) /\ (h . B) ; ::_thesis: m in x
then A21: m in h . B by XBOOLE_0:def_4;
m in h . A by A20, XBOOLE_0:def_4;
then for y being set st y in rng h holds
m in y by A21, A15, TARSKI:def_2;
hence m in x by A8, A12, A13, SETFAM_1:def_1; ::_thesis: verum
end;
A22: B in G by A2, TARSKI:def_2;
then A23: h . B in B by A7;
A24: h . B in rng h by A5, A22, FUNCT_1:def_3;
x c= (h . A) /\ (h . B)
proof
let m be set ; :: according to TARSKI:def_3 ::_thesis: ( not m in x or m in (h . A) /\ (h . B) )
assume A25: m in x ; ::_thesis: m in (h . A) /\ (h . B)
then A26: m in h . B by A8, A24, A13, SETFAM_1:def_1;
m in h . A by A8, A12, A13, A25, SETFAM_1:def_1;
hence m in (h . A) /\ (h . B) by A26, XBOOLE_0:def_4; ::_thesis: verum
end;
then A27: (h . A) /\ (h . B) = x by A14, XBOOLE_0:def_10;
h . A in A by A7, A11;
then x in INTERSECTION (A,B) by A23, A27, SETFAM_1:def_5;
then x in (INTERSECTION (A,B)) \ {{}} by A10, XBOOLE_0:def_5;
hence x in A '/\' B by PARTIT1:def_4; ::_thesis: verum
end;
A '/\' B c= '/\' G
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A '/\' B or x in '/\' G )
assume x in A '/\' B ; ::_thesis: x in '/\' G
then x in (INTERSECTION (A,B)) \ {{}} by PARTIT1:def_4;
then consider X, Z being set such that
A28: X in A and
A29: Z in B and
A30: x = X /\ Z by SETFAM_1:def_5;
{X,Z} c= bool Y
proof
let m be set ; :: according to TARSKI:def_3 ::_thesis: ( not m in {X,Z} or m in bool Y )
assume m in {X,Z} ; ::_thesis: m in bool Y
then ( m = X or m = Z ) by TARSKI:def_2;
hence m in bool Y by A28, A29; ::_thesis: verum
end;
then reconsider SS = {X,Z} as Subset-Family of Y ;
A31: X /\ Z = Intersect SS by A28, A29, MSSUBFAM:10;
set h = (A,B) --> (X,Z);
A32: for d being set st d in G holds
((A,B) --> (X,Z)) . d in d
proof
let d be set ; ::_thesis: ( d in G implies ((A,B) --> (X,Z)) . d in d )
assume d in G ; ::_thesis: ((A,B) --> (X,Z)) . d in d
then ( d = A or d = B ) by A2, TARSKI:def_2;
hence ((A,B) --> (X,Z)) . d in d by A3, A28, A29, FUNCT_4:63; ::_thesis: verum
end;
A33: dom ((A,B) --> (X,Z)) = {A,B} by FUNCT_4:62;
A34: rng ((A,B) --> (X,Z)) = SS by A3, FUNCT_4:64;
then Intersect SS <> {} by A1, A2, A33, A32, BVFUNC_2:def_5;
hence x in '/\' G by A2, A30, A33, A34, A32, A31, BVFUNC_2:def_1; ::_thesis: verum
end;
hence '/\' G = A '/\' B by A4, XBOOLE_0:def_10; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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
let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y st G = {A,B} & A <> B holds
CompF (A,G) = B
let A, B be a_partition of Y; ::_thesis: ( G = {A,B} & A <> B implies CompF (A,G) = B )
assume that
A1: G = {A,B} and
A2: A <> B ; ::_thesis: CompF (A,G) = B
A3: '/\' {B} c= B
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in '/\' {B} or x in B )
assume x in '/\' {B} ; ::_thesis: x in B
then consider h being Function, F being Subset-Family of Y such that
A4: dom h = {B} and
A5: rng h = F and
A6: for d being set st d in {B} holds
h . d in d and
A7: x = Intersect F and
x <> {} by BVFUNC_2:def_1;
rng h = {(h . B)} by A4, FUNCT_1:4;
then A8: x = meet {(h . B)} by A5, A7, SETFAM_1:def_9;
B in {B} by TARSKI:def_1;
then h . B in B by A6;
hence x in B by A8, SETFAM_1:10; ::_thesis: verum
end;
A9: B c= '/\' {B}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B or x in '/\' {B} )
set h0 = B .--> x;
A10: dom (B .--> x) = {B} by FUNCOP_1:13;
assume A11: x in B ; ::_thesis: x in '/\' {B}
A12: for d being set st d in {B} holds
(B .--> x) . d in d
proof
let d be set ; ::_thesis: ( d in {B} implies (B .--> x) . d in d )
assume d in {B} ; ::_thesis: (B .--> x) . d in d
then d = B by TARSKI:def_1;
hence (B .--> x) . d in d by A11, FUNCOP_1:72; ::_thesis: verum
end;
A13: rng (B .--> x) = {x} by FUNCOP_1:8;
rng (B .--> x) c= bool Y
proof
let m be set ; :: according to TARSKI:def_3 ::_thesis: ( not m in rng (B .--> x) or m in bool Y )
assume m in rng (B .--> x) ; ::_thesis: m in bool Y
then m = x by A13, TARSKI:def_1;
hence m in bool Y by A11; ::_thesis: verum
end;
then reconsider F0 = rng (B .--> x) as Subset-Family of Y ;
meet F0 = Intersect F0 by A13, SETFAM_1:def_9;
then A14: x = Intersect F0 by A13, SETFAM_1:10;
x <> {} by A11, EQREL_1:def_4;
hence x in '/\' {B} by A10, A12, A14, BVFUNC_2:def_1; ::_thesis: verum
end;
A in {A} by TARSKI:def_1;
then A15: {A} \ {A} = {} by ZFMISC_1:60;
G \ {A} = ({A} \/ {B}) \ {A} by A1, ENUMSET1:1
.= ({A} \ {A}) \/ ({B} \ {A}) by XBOOLE_1:42
.= ({A} \ {A}) \/ {B} by A2, ZFMISC_1:14 ;
then CompF (A,G) = '/\' {B} by A15, BVFUNC_2:def_7;
hence CompF (A,G) = B by A3, A9, XBOOLE_0:def_10; ::_thesis: verum
end;
begin
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
let Y be non empty set ; ::_thesis: 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)
let a, b be Function of Y,BOOLEAN; ::_thesis: 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)
let G be Subset of (PARTITIONS Y); ::_thesis: for A being a_partition of Y st a '<' b holds
All (a,A,G) '<' Ex (b,A,G)
let A be a_partition of Y; ::_thesis: ( a '<' b implies All (a,A,G) '<' Ex (b,A,G) )
assume a '<' b ; ::_thesis: All (a,A,G) '<' Ex (b,A,G)
then A1: All (a,A,G) '<' All (b,A,G) by PARTIT_2:12;
All (b,A,G) '<' Ex (b,A,G) by BVFUNC_4:17;
hence All (a,A,G) '<' Ex (b,A,G) by A1, BVFUNC_1:15; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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)
let a be Function of Y,BOOLEAN; ::_thesis: 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)
let G be Subset of (PARTITIONS Y); ::_thesis: 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)
let A, B be a_partition of Y; ::_thesis: ( G is independent implies All ((All (a,A,G)),B,G) '<' Ex ((All (a,B,G)),A,G) )
assume G is independent ; ::_thesis: All ((All (a,A,G)),B,G) '<' Ex ((All (a,B,G)),A,G)
then All ((All (a,A,G)),B,G) = All ((All (a,B,G)),A,G) by PARTIT_2:15;
hence All ((All (a,A,G)),B,G) '<' Ex ((All (a,B,G)),A,G) by Th8; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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)
let a be Function of Y,BOOLEAN; ::_thesis: 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)
let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y holds All ((All (a,A,G)),B,G) '<' Ex ((Ex (a,B,G)),A,G)
let A, B be a_partition of Y; ::_thesis: All ((All (a,A,G)),B,G) '<' Ex ((Ex (a,B,G)),A,G)
A1: All ((All (a,A,G)),B,G) '<' All (a,A,G) by BVFUNC_2:11;
All (a,A,G) '<' Ex ((Ex (a,B,G)),A,G) by Th8, BVFUNC_2:12;
hence All ((All (a,A,G)),B,G) '<' Ex ((Ex (a,B,G)),A,G) by A1, BVFUNC_1:15; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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)
let a be Function of Y,BOOLEAN; ::_thesis: 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)
let G be Subset of (PARTITIONS Y); ::_thesis: 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)
let A, B be a_partition of Y; ::_thesis: ( G is independent implies All ((All (a,A,G)),B,G) '<' All ((Ex (a,B,G)),A,G) )
assume G is independent ; ::_thesis: All ((All (a,A,G)),B,G) '<' All ((Ex (a,B,G)),A,G)
then A1: All ((All (a,A,G)),B,G) = All ((All (a,B,G)),A,G) by PARTIT_2:15;
All (a,B,G) '<' Ex (a,B,G) by Th8;
hence All ((All (a,A,G)),B,G) '<' All ((Ex (a,B,G)),A,G) by A1, PARTIT_2:12; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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)
let a be Function of Y,BOOLEAN; ::_thesis: 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)
let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y holds All ((Ex (a,A,G)),B,G) '<' Ex ((Ex (a,B,G)),A,G)
let A, B be a_partition of Y; ::_thesis: All ((Ex (a,A,G)),B,G) '<' Ex ((Ex (a,B,G)),A,G)
A1: Ex (a,B,G) = B_SUP (a,(CompF (B,G))) by BVFUNC_2:def_10;
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (All ((Ex (a,A,G)),B,G)) . z = TRUE or (Ex ((Ex (a,B,G)),A,G)) . z = TRUE )
assume A2: (All ((Ex (a,A,G)),B,G)) . z = TRUE ; ::_thesis: (Ex ((Ex (a,B,G)),A,G)) . z = TRUE
A3: now__::_thesis:_for_x_being_Element_of_Y_st_x_in_EqClass_(z,(CompF_(B,G)))_holds_
(Ex_(a,A,G))_._x_=_TRUE
assume ex x being Element of Y st
( x in EqClass (z,(CompF (B,G))) & not (Ex (a,A,G)) . x = TRUE ) ; ::_thesis: contradiction
then (B_INF ((Ex (a,A,G)),(CompF (B,G)))) . z = FALSE by BVFUNC_1:def_16;
hence contradiction by A2, BVFUNC_2:def_9; ::_thesis: verum
end;
A4: z in EqClass (z,(CompF (B,G))) by EQREL_1:def_6;
now__::_thesis:_ex_x_being_Element_of_Y_st_
(_x_in_EqClass_(z,(CompF_(A,G)))_&_a_._x_=_TRUE_)
assume for x being Element of Y holds
( not x in EqClass (z,(CompF (A,G))) or not a . x = TRUE ) ; ::_thesis: contradiction
then (B_SUP (a,(CompF (A,G)))) . z = FALSE by BVFUNC_1:def_17;
then (Ex (a,A,G)) . z = FALSE by BVFUNC_2:def_10;
hence contradiction by A4, A3; ::_thesis: verum
end;
then consider x1 being Element of Y such that
A5: x1 in EqClass (z,(CompF (A,G))) and
A6: a . x1 = TRUE ;
x1 in EqClass (x1,(CompF (B,G))) by EQREL_1:def_6;
then (Ex (a,B,G)) . x1 = TRUE by A1, A6, BVFUNC_1:def_17;
then (B_SUP ((Ex (a,B,G)),(CompF (A,G)))) . z = TRUE by A5, BVFUNC_1:def_17;
hence (Ex ((Ex (a,B,G)),A,G)) . z = TRUE by BVFUNC_2:def_10; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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)
let a be Function of Y,BOOLEAN; ::_thesis: 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)
let G be Subset of (PARTITIONS Y); ::_thesis: 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)
let A, B be a_partition of Y; ::_thesis: 'not' (Ex ((All (a,A,G)),B,G)) '<' Ex ((Ex (('not' a),B,G)),A,G)
A1: All (a,A,G) = B_INF (a,(CompF (A,G))) by BVFUNC_2:def_9;
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ('not' (Ex ((All (a,A,G)),B,G))) . z = TRUE or (Ex ((Ex (('not' a),B,G)),A,G)) . z = TRUE )
A2: z in EqClass (z,(CompF (B,G))) by EQREL_1:def_6;
assume ('not' (Ex ((All (a,A,G)),B,G))) . z = TRUE ; ::_thesis: (Ex ((Ex (('not' a),B,G)),A,G)) . z = TRUE
then A3: 'not' ((Ex ((All (a,A,G)),B,G)) . z) = TRUE by MARGREL1:def_19;
Ex ((All (a,A,G)),B,G) = B_SUP ((All (a,A,G)),(CompF (B,G))) by BVFUNC_2:def_10;
then (All (a,A,G)) . z <> TRUE by A3, A2, BVFUNC_1:def_17;
then consider x1 being Element of Y such that
A4: x1 in EqClass (z,(CompF (A,G))) and
A5: a . x1 <> TRUE by A1, BVFUNC_1:def_16;
a . x1 = FALSE by A5, XBOOLEAN:def_3;
then A6: ('not' a) . x1 = 'not' FALSE by MARGREL1:def_19;
A7: Ex (('not' a),B,G) = B_SUP (('not' a),(CompF (B,G))) by BVFUNC_2:def_10;
x1 in EqClass (x1,(CompF (B,G))) by EQREL_1:def_6;
then (Ex (('not' a),B,G)) . x1 = TRUE by A7, A6, BVFUNC_1:def_17;
then (B_SUP ((Ex (('not' a),B,G)),(CompF (A,G)))) . z = TRUE by A4, BVFUNC_1:def_17;
hence (Ex ((Ex (('not' a),B,G)),A,G)) . z = TRUE by BVFUNC_2:def_10; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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)
let a be Function of Y,BOOLEAN; ::_thesis: 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)
let G be Subset of (PARTITIONS Y); ::_thesis: 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)
let A, B be a_partition of Y; ::_thesis: ( G is independent implies Ex (('not' (All (a,A,G))),B,G) '<' Ex ((Ex (('not' a),B,G)),A,G) )
assume G is independent ; ::_thesis: Ex (('not' (All (a,A,G))),B,G) '<' Ex ((Ex (('not' a),B,G)),A,G)
then Ex ((Ex (('not' a),B,G)),A,G) = Ex ((Ex (('not' a),A,G)),B,G) by PARTIT_2:16;
hence Ex (('not' (All (a,A,G))),B,G) '<' Ex ((Ex (('not' a),B,G)),A,G) by BVFUNC_2:18; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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)
let a be Function of Y,BOOLEAN; ::_thesis: 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)
let G be Subset of (PARTITIONS Y); ::_thesis: 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)
let A, B be a_partition of Y; ::_thesis: ( G is independent implies 'not' (All ((All (a,A,G)),B,G)) = Ex (('not' (All (a,B,G))),A,G) )
assume G is independent ; ::_thesis: 'not' (All ((All (a,A,G)),B,G)) = Ex (('not' (All (a,B,G))),A,G)
then All ((All (a,A,G)),B,G) = All ((All (a,B,G)),A,G) by PARTIT_2:15;
hence 'not' (All ((All (a,A,G)),B,G)) = Ex (('not' (All (a,B,G))),A,G) by BVFUNC_2:18; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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)
let a be Function of Y,BOOLEAN; ::_thesis: 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)
let G be Subset of (PARTITIONS Y); ::_thesis: 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)
let A, B be a_partition of Y; ::_thesis: ( G is independent implies All (('not' (All (a,A,G))),B,G) '<' Ex ((Ex (('not' a),B,G)),A,G) )
assume G is independent ; ::_thesis: All (('not' (All (a,A,G))),B,G) '<' Ex ((Ex (('not' a),B,G)),A,G)
then A1: Ex ((Ex (('not' a),B,G)),A,G) = Ex ((Ex (('not' a),A,G)),B,G) by PARTIT_2:16;
'not' (All (a,A,G)) = Ex (('not' a),A,G) by BVFUNC_2:18;
hence All (('not' (All (a,A,G))),B,G) '<' Ex ((Ex (('not' a),B,G)),A,G) by A1, Th8; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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)
let a be Function of Y,BOOLEAN; ::_thesis: 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)
let G be Subset of (PARTITIONS Y); ::_thesis: 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)
let A, B be a_partition of Y; ::_thesis: ( G is independent implies 'not' (All ((All (a,A,G)),B,G)) = Ex ((Ex (('not' a),B,G)),A,G) )
A1: Ex (('not' a),B,G) = 'not' (All (a,B,G)) by BVFUNC_2:18;
assume G is independent ; ::_thesis: 'not' (All ((All (a,A,G)),B,G)) = Ex ((Ex (('not' a),B,G)),A,G)
hence 'not' (All ((All (a,A,G)),B,G)) = Ex ((Ex (('not' a),B,G)),A,G) by A1, Th15; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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)
let a be Function of Y,BOOLEAN; ::_thesis: 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)
let G be Subset of (PARTITIONS Y); ::_thesis: 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)
let A, B be a_partition of Y; ::_thesis: ( G is independent implies 'not' (All ((All (a,A,G)),B,G)) '<' Ex ((Ex (('not' a),A,G)),B,G) )
assume A1: G is independent ; ::_thesis: 'not' (All ((All (a,A,G)),B,G)) '<' Ex ((Ex (('not' a),A,G)),B,G)
then Ex (('not' (All (a,B,G))),A,G) '<' Ex ((Ex (('not' a),A,G)),B,G) by Th14;
hence 'not' (All ((All (a,A,G)),B,G)) '<' Ex ((Ex (('not' a),A,G)),B,G) by A1, Th15; ::_thesis: verum
end;
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
let Y be non empty set ; ::_thesis: 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)
let a be Function of Y,BOOLEAN; ::_thesis: 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)
let G be Subset of (PARTITIONS Y); ::_thesis: 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)
let A, B be a_partition of Y; ::_thesis: 'not' (All ((Ex (a,A,G)),B,G)) = Ex ((All (('not' a),A,G)),B,G)
'not' (All ((Ex (a,A,G)),B,G)) = Ex (('not' (Ex (a,A,G))),B,G) by BVFUNC_2:18;
hence 'not' (All ((Ex (a,A,G)),B,G)) = Ex ((All (('not' a),A,G)),B,G) by BVFUNC_2:19; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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)
let a be Function of Y,BOOLEAN; ::_thesis: 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)
let G be Subset of (PARTITIONS Y); ::_thesis: 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)
let A, B be a_partition of Y; ::_thesis: 'not' (Ex ((All (a,A,G)),B,G)) = All ((Ex (('not' a),A,G)),B,G)
'not' (Ex ((All (a,A,G)),B,G)) = All (('not' (All (a,A,G))),B,G) by BVFUNC_2:19;
hence 'not' (Ex ((All (a,A,G)),B,G)) = All ((Ex (('not' a),A,G)),B,G) by BVFUNC_2:18; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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)
let a be Function of Y,BOOLEAN; ::_thesis: 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)
let G be Subset of (PARTITIONS Y); ::_thesis: 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)
let A, B be a_partition of Y; ::_thesis: 'not' (All ((All (a,A,G)),B,G)) = Ex ((Ex (('not' a),A,G)),B,G)
Ex (('not' (All (a,A,G))),B,G) = Ex ((Ex (('not' a),A,G)),B,G) by BVFUNC_2:18;
hence 'not' (All ((All (a,A,G)),B,G)) = Ex ((Ex (('not' a),A,G)),B,G) by BVFUNC_2:18; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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)
let a be Function of Y,BOOLEAN; ::_thesis: 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)
let G be Subset of (PARTITIONS Y); ::_thesis: 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)
let A, B be a_partition of Y; ::_thesis: ( G is independent implies Ex ((All (a,A,G)),B,G) '<' Ex ((Ex (a,B,G)),A,G) )
assume G is independent ; ::_thesis: Ex ((All (a,A,G)),B,G) '<' Ex ((Ex (a,B,G)),A,G)
then A1: Ex ((Ex (a,B,G)),A,G) = Ex ((Ex (a,A,G)),B,G) by PARTIT_2:16;
All (a,A,G) '<' Ex (a,A,G) by Th8;
hence Ex ((All (a,A,G)),B,G) '<' Ex ((Ex (a,B,G)),A,G) by A1, PARTIT_2:13; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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)
let a be Function of Y,BOOLEAN; ::_thesis: 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)
let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y holds All ((All (a,A,G)),B,G) '<' All ((Ex (a,A,G)),B,G)
let A, B be a_partition of Y; ::_thesis: All ((All (a,A,G)),B,G) '<' All ((Ex (a,A,G)),B,G)
All (a,A,G) '<' Ex (a,A,G) by Th8;
hence All ((All (a,A,G)),B,G) '<' All ((Ex (a,A,G)),B,G) by PARTIT_2:12; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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)
let a be Function of Y,BOOLEAN; ::_thesis: 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)
let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y holds All ((All (a,A,G)),B,G) '<' Ex ((Ex (a,A,G)),B,G)
let A, B be a_partition of Y; ::_thesis: All ((All (a,A,G)),B,G) '<' Ex ((Ex (a,A,G)),B,G)
All (a,A,G) '<' Ex (a,A,G) by Th8;
hence All ((All (a,A,G)),B,G) '<' Ex ((Ex (a,A,G)),B,G) by Th8; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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)
let a be Function of Y,BOOLEAN; ::_thesis: 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)
let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y holds Ex ((All (a,A,G)),B,G) '<' Ex ((Ex (a,A,G)),B,G)
let A, B be a_partition of Y; ::_thesis: Ex ((All (a,A,G)),B,G) '<' Ex ((Ex (a,A,G)),B,G)
All (a,A,G) '<' Ex (a,A,G) by Th8;
hence Ex ((All (a,A,G)),B,G) '<' Ex ((Ex (a,A,G)),B,G) by PARTIT_2:13; ::_thesis: verum
end;
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
let Y be non empty set ; ::_thesis: 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))
let a be Function of Y,BOOLEAN; ::_thesis: 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))
let G be Subset of (PARTITIONS Y); ::_thesis: 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))
let A, B be a_partition of Y; ::_thesis: ( G is independent implies All (('not' (All (a,A,G))),B,G) '<' 'not' (All ((All (a,B,G)),A,G)) )
assume G is independent ; ::_thesis: All (('not' (All (a,A,G))),B,G) '<' 'not' (All ((All (a,B,G)),A,G))
then All ((All (a,B,G)),A,G) = All ((All (a,A,G)),B,G) by PARTIT_2:15;
then ( All (('not' (All (a,A,G))),B,G) = 'not' (Ex ((All (a,A,G)),B,G)) & All ((All (a,B,G)),A,G) '<' Ex ((All (a,A,G)),B,G) ) by Th8, BVFUNC_2:19;
hence All (('not' (All (a,A,G))),B,G) '<' 'not' (All ((All (a,B,G)),A,G)) by PARTIT_2:11; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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))
let a be Function of Y,BOOLEAN; ::_thesis: 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))
let G be Subset of (PARTITIONS Y); ::_thesis: 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))
let A, B be a_partition of Y; ::_thesis: All ((All (('not' a),A,G)),B,G) '<' 'not' (All ((All (a,B,G)),A,G))
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (All ((All (('not' a),A,G)),B,G)) . z = TRUE or ('not' (All ((All (a,B,G)),A,G))) . z = TRUE )
A1: z in EqClass (z,(CompF (A,G))) by EQREL_1:def_6;
A2: z in EqClass (z,(CompF (B,G))) by EQREL_1:def_6;
assume A3: (All ((All (('not' a),A,G)),B,G)) . z = TRUE ; ::_thesis: ('not' (All ((All (a,B,G)),A,G))) . z = TRUE
now__::_thesis:_for_x_being_Element_of_Y_st_x_in_EqClass_(z,(CompF_(B,G)))_holds_
(All_(('not'_a),A,G))_._x_=_TRUE
assume ex x being Element of Y st
( x in EqClass (z,(CompF (B,G))) & not (All (('not' a),A,G)) . x = TRUE ) ; ::_thesis: contradiction
then (B_INF ((All (('not' a),A,G)),(CompF (B,G)))) . z = FALSE by BVFUNC_1:def_16;
hence contradiction by A3, BVFUNC_2:def_9; ::_thesis: verum
end;
then ( All (('not' a),A,G) = B_INF (('not' a),(CompF (A,G))) & (All (('not' a),A,G)) . z = TRUE ) by A2, BVFUNC_2:def_9;
then ('not' a) . z = TRUE by A1, BVFUNC_1:def_16;
then 'not' (a . z) = TRUE by MARGREL1:def_19;
then (B_INF (a,(CompF (B,G)))) . z = FALSE by A2, BVFUNC_1:def_16;
then (All (a,B,G)) . z = FALSE by BVFUNC_2:def_9;
then (B_INF ((All (a,B,G)),(CompF (A,G)))) . z = FALSE by A1, BVFUNC_1:def_16;
then (All ((All (a,B,G)),A,G)) . z = FALSE by BVFUNC_2:def_9;
then 'not' ((All ((All (a,B,G)),A,G)) . z) = TRUE ;
hence ('not' (All ((All (a,B,G)),A,G))) . z = TRUE by MARGREL1:def_19; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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))
let a be Function of Y,BOOLEAN; ::_thesis: 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))
let G be Subset of (PARTITIONS Y); ::_thesis: 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))
let A, B be a_partition of Y; ::_thesis: All (('not' (Ex (a,A,G))),B,G) '<' 'not' (All ((All (a,B,G)),A,G))
All (('not' (Ex (a,A,G))),B,G) = All ((All (('not' a),A,G)),B,G) by BVFUNC_2:19;
hence All (('not' (Ex (a,A,G))),B,G) '<' 'not' (All ((All (a,B,G)),A,G)) by Th27; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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))
let a be Function of Y,BOOLEAN; ::_thesis: 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))
let G be Subset of (PARTITIONS Y); ::_thesis: 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))
let A, B be a_partition of Y; ::_thesis: ( G is independent implies All ((Ex (('not' a),A,G)),B,G) '<' 'not' (All ((All (a,B,G)),A,G)) )
Ex (('not' a),A,G) = 'not' (All (a,A,G)) by BVFUNC_2:18;
then A1: All ((Ex (('not' a),A,G)),B,G) = 'not' (Ex ((All (a,A,G)),B,G)) by BVFUNC_2:19;
assume G is independent ; ::_thesis: All ((Ex (('not' a),A,G)),B,G) '<' 'not' (All ((All (a,B,G)),A,G))
hence All ((Ex (('not' a),A,G)),B,G) '<' 'not' (All ((All (a,B,G)),A,G)) by A1, Th9, PARTIT_2:11; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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))
let a be Function of Y,BOOLEAN; ::_thesis: 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))
let G be Subset of (PARTITIONS Y); ::_thesis: 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))
let A, B be a_partition of Y; ::_thesis: ( G is independent implies Ex ((All (('not' a),A,G)),B,G) '<' 'not' (All ((All (a,B,G)),A,G)) )
assume A1: G is independent ; ::_thesis: Ex ((All (('not' a),A,G)),B,G) '<' 'not' (All ((All (a,B,G)),A,G))
then ( Ex ((All (('not' a),A,G)),B,G) '<' All ((Ex (('not' a),B,G)),A,G) & All ((Ex (('not' a),B,G)),A,G) '<' 'not' (All ((All (a,A,G)),B,G)) ) by Th29, PARTIT_2:17;
then Ex ((All (('not' a),A,G)),B,G) '<' 'not' (All ((All (a,A,G)),B,G)) by BVFUNC_1:15;
hence Ex ((All (('not' a),A,G)),B,G) '<' 'not' (All ((All (a,B,G)),A,G)) by A1, PARTIT_2:15; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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))
let a be Function of Y,BOOLEAN; ::_thesis: 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))
let G be Subset of (PARTITIONS Y); ::_thesis: 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))
let A, B be a_partition of Y; ::_thesis: ( G is independent implies Ex (('not' (Ex (a,A,G))),B,G) '<' 'not' (All ((All (a,B,G)),A,G)) )
All (a,A,G) '<' Ex (a,A,G) by Th8;
then A1: All ((All (a,A,G)),B,G) '<' All ((Ex (a,A,G)),B,G) by PARTIT_2:12;
assume G is independent ; ::_thesis: Ex (('not' (Ex (a,A,G))),B,G) '<' 'not' (All ((All (a,B,G)),A,G))
then ( Ex (('not' (Ex (a,A,G))),B,G) = 'not' (All ((Ex (a,A,G)),B,G)) & All ((All (a,B,G)),A,G) = All ((All (a,A,G)),B,G) ) by BVFUNC_2:18, PARTIT_2:15;
hence Ex (('not' (Ex (a,A,G))),B,G) '<' 'not' (All ((All (a,B,G)),A,G)) by A1, PARTIT_2:11; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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))
let a be Function of Y,BOOLEAN; ::_thesis: 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))
let G be Subset of (PARTITIONS Y); ::_thesis: 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))
let A, B be a_partition of Y; ::_thesis: ( G is independent implies 'not' (Ex ((Ex (a,A,G)),B,G)) '<' 'not' (Ex ((All (a,B,G)),A,G)) )
assume G is independent ; ::_thesis: 'not' (Ex ((Ex (a,A,G)),B,G)) '<' 'not' (Ex ((All (a,B,G)),A,G))
then A1: Ex ((Ex (a,A,G)),B,G) = Ex ((Ex (a,B,G)),A,G) by PARTIT_2:16;
All (a,B,G) '<' Ex (a,B,G) by Th8;
then Ex ((All (a,B,G)),A,G) '<' Ex ((Ex (a,A,G)),B,G) by A1, PARTIT_2:13;
hence 'not' (Ex ((Ex (a,A,G)),B,G)) '<' 'not' (Ex ((All (a,B,G)),A,G)) by PARTIT_2:11; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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))
let a be Function of Y,BOOLEAN; ::_thesis: 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))
let G be Subset of (PARTITIONS Y); ::_thesis: 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))
let A, B be a_partition of Y; ::_thesis: 'not' (Ex ((Ex (a,A,G)),B,G)) '<' 'not' (All ((Ex (a,B,G)),A,G))
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ('not' (Ex ((Ex (a,A,G)),B,G))) . z = TRUE or ('not' (All ((Ex (a,B,G)),A,G))) . z = TRUE )
assume ('not' (Ex ((Ex (a,A,G)),B,G))) . z = TRUE ; ::_thesis: ('not' (All ((Ex (a,B,G)),A,G))) . z = TRUE
then A1: 'not' ((Ex ((Ex (a,A,G)),B,G)) . z) = TRUE by MARGREL1:def_19;
A2: now__::_thesis:_for_x_being_Element_of_Y_holds_
(_not_x_in_EqClass_(z,(CompF_(B,G)))_or_not_(Ex_(a,A,G))_._x_=_TRUE_)
assume ex x being Element of Y st
( x in EqClass (z,(CompF (B,G))) & (Ex (a,A,G)) . x = TRUE ) ; ::_thesis: contradiction
then (B_SUP ((Ex (a,A,G)),(CompF (B,G)))) . z = TRUE by BVFUNC_1:def_17;
then (Ex ((Ex (a,A,G)),B,G)) . z = TRUE by BVFUNC_2:def_10;
hence contradiction by A1; ::_thesis: verum
end;
A3: Ex (a,A,G) = B_SUP (a,(CompF (A,G))) by BVFUNC_2:def_10;
A4: for x being Element of Y st x in EqClass (z,(CompF (B,G))) holds
for y being Element of Y st y in EqClass (x,(CompF (A,G))) holds
a . y <> TRUE
proof
let x be Element of Y; ::_thesis: ( x in EqClass (z,(CompF (B,G))) implies for y being Element of Y st y in EqClass (x,(CompF (A,G))) holds
a . y <> TRUE )
assume x in EqClass (z,(CompF (B,G))) ; ::_thesis: for y being Element of Y st y in EqClass (x,(CompF (A,G))) holds
a . y <> TRUE
then (Ex (a,A,G)) . x <> TRUE by A2;
hence for y being Element of Y st y in EqClass (x,(CompF (A,G))) holds
a . y <> TRUE by A3, BVFUNC_1:def_17; ::_thesis: verum
end;
for x being Element of Y st x in EqClass (z,(CompF (B,G))) holds
a . x <> TRUE
proof
let x be Element of Y; ::_thesis: ( x in EqClass (z,(CompF (B,G))) implies a . x <> TRUE )
A5: x in EqClass (x,(CompF (A,G))) by EQREL_1:def_6;
assume x in EqClass (z,(CompF (B,G))) ; ::_thesis: a . x <> TRUE
hence a . x <> TRUE by A4, A5; ::_thesis: verum
end;
then (B_SUP (a,(CompF (B,G)))) . z = FALSE by BVFUNC_1:def_17;
then ( z in EqClass (z,(CompF (A,G))) & (Ex (a,B,G)) . z = FALSE ) by BVFUNC_2:def_10, EQREL_1:def_6;
then (B_INF ((Ex (a,B,G)),(CompF (A,G)))) . z = FALSE by BVFUNC_1:def_16;
then (All ((Ex (a,B,G)),A,G)) . z = FALSE by BVFUNC_2:def_9;
then 'not' ((All ((Ex (a,B,G)),A,G)) . z) = TRUE ;
hence ('not' (All ((Ex (a,B,G)),A,G))) . z = TRUE by MARGREL1:def_19; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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))
let a be Function of Y,BOOLEAN; ::_thesis: 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))
let G be Subset of (PARTITIONS Y); ::_thesis: 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))
let A, B be a_partition of Y; ::_thesis: ( G is independent implies 'not' (Ex ((All (a,A,G)),B,G)) '<' 'not' (All ((All (a,B,G)),A,G)) )
assume G is independent ; ::_thesis: 'not' (Ex ((All (a,A,G)),B,G)) '<' 'not' (All ((All (a,B,G)),A,G))
then All (('not' (All (a,A,G))),B,G) '<' 'not' (All ((All (a,B,G)),A,G)) by Th26;
hence 'not' (Ex ((All (a,A,G)),B,G)) '<' 'not' (All ((All (a,B,G)),A,G)) by BVFUNC_2:19; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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))
let a be Function of Y,BOOLEAN; ::_thesis: 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))
let G be Subset of (PARTITIONS Y); ::_thesis: 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))
let A, B be a_partition of Y; ::_thesis: ( G is independent implies 'not' (All ((Ex (a,A,G)),B,G)) '<' 'not' (All ((All (a,B,G)),A,G)) )
assume G is independent ; ::_thesis: 'not' (All ((Ex (a,A,G)),B,G)) '<' 'not' (All ((All (a,B,G)),A,G))
then A1: Ex (('not' (Ex (a,A,G))),B,G) '<' 'not' (All ((All (a,B,G)),A,G)) by Th31;
Ex (('not' (Ex (a,A,G))),B,G) = Ex ((All (('not' a),A,G)),B,G) by BVFUNC_2:19;
hence 'not' (All ((Ex (a,A,G)),B,G)) '<' 'not' (All ((All (a,B,G)),A,G)) by A1, Th19; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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))
let a be Function of Y,BOOLEAN; ::_thesis: 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))
let G be Subset of (PARTITIONS Y); ::_thesis: 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))
let A, B be a_partition of Y; ::_thesis: 'not' (Ex ((Ex (a,A,G)),B,G)) '<' 'not' (All ((All (a,B,G)),A,G))
All (('not' (Ex (a,A,G))),B,G) '<' 'not' (All ((All (a,B,G)),A,G)) by Th28;
hence 'not' (Ex ((Ex (a,A,G)),B,G)) '<' 'not' (All ((All (a,B,G)),A,G)) by BVFUNC_2:19; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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)
let a be Function of Y,BOOLEAN; ::_thesis: 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)
let G be Subset of (PARTITIONS Y); ::_thesis: 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)
let A, B be a_partition of Y; ::_thesis: ( G is independent implies 'not' (Ex ((All (a,A,G)),B,G)) '<' Ex (('not' (All (a,B,G))),A,G) )
assume G is independent ; ::_thesis: 'not' (Ex ((All (a,A,G)),B,G)) '<' Ex (('not' (All (a,B,G))),A,G)
then A1: All (('not' (All (a,A,G))),B,G) '<' 'not' (All ((All (a,B,G)),A,G)) by Th26;
'not' (Ex ((All (a,A,G)),B,G)) = All (('not' (All (a,A,G))),B,G) by BVFUNC_2:19;
hence 'not' (Ex ((All (a,A,G)),B,G)) '<' Ex (('not' (All (a,B,G))),A,G) by A1, BVFUNC_2:18; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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)
let a be Function of Y,BOOLEAN; ::_thesis: 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)
let G be Subset of (PARTITIONS Y); ::_thesis: 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)
let A, B be a_partition of Y; ::_thesis: ( G is independent implies 'not' (All ((Ex (a,A,G)),B,G)) '<' Ex (('not' (All (a,B,G))),A,G) )
assume G is independent ; ::_thesis: 'not' (All ((Ex (a,A,G)),B,G)) '<' Ex (('not' (All (a,B,G))),A,G)
then A1: Ex (('not' (Ex (a,A,G))),B,G) '<' 'not' (All ((All (a,B,G)),A,G)) by Th31;
( 'not' (All ((Ex (a,A,G)),B,G)) = Ex ((All (('not' a),A,G)),B,G) & Ex (('not' (Ex (a,A,G))),B,G) = Ex ((All (('not' a),A,G)),B,G) ) by Th19, BVFUNC_2:19;
hence 'not' (All ((Ex (a,A,G)),B,G)) '<' Ex (('not' (All (a,B,G))),A,G) by A1, BVFUNC_2:18; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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)
let a be Function of Y,BOOLEAN; ::_thesis: 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)
let G be Subset of (PARTITIONS Y); ::_thesis: 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)
let A, B be a_partition of Y; ::_thesis: 'not' (Ex ((Ex (a,A,G)),B,G)) '<' Ex (('not' (All (a,B,G))),A,G)
( All (('not' (Ex (a,A,G))),B,G) '<' 'not' (All ((All (a,B,G)),A,G)) & 'not' (Ex ((Ex (a,A,G)),B,G)) = All (('not' (Ex (a,A,G))),B,G) ) by Th28, BVFUNC_2:19;
hence 'not' (Ex ((Ex (a,A,G)),B,G)) '<' Ex (('not' (All (a,B,G))),A,G) by BVFUNC_2:18; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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)
let a be Function of Y,BOOLEAN; ::_thesis: 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)
let G be Subset of (PARTITIONS Y); ::_thesis: 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)
let A, B be a_partition of Y; ::_thesis: ( G is independent implies 'not' (All ((Ex (a,A,G)),B,G)) '<' All (('not' (All (a,B,G))),A,G) )
assume G is independent ; ::_thesis: 'not' (All ((Ex (a,A,G)),B,G)) '<' All (('not' (All (a,B,G))),A,G)
then 'not' (All ((Ex (a,A,G)),B,G)) '<' 'not' (Ex ((All (a,B,G)),A,G)) by PARTIT_2:11, PARTIT_2:17;
hence 'not' (All ((Ex (a,A,G)),B,G)) '<' All (('not' (All (a,B,G))),A,G) by BVFUNC_2:19; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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)
let a be Function of Y,BOOLEAN; ::_thesis: 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)
let G be Subset of (PARTITIONS Y); ::_thesis: 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)
let A, B be a_partition of Y; ::_thesis: ( G is independent implies 'not' (Ex ((Ex (a,A,G)),B,G)) '<' All (('not' (All (a,B,G))),A,G) )
assume G is independent ; ::_thesis: 'not' (Ex ((Ex (a,A,G)),B,G)) '<' All (('not' (All (a,B,G))),A,G)
then 'not' (Ex ((Ex (a,A,G)),B,G)) '<' 'not' (Ex ((All (a,B,G)),A,G)) by Th33;
hence 'not' (Ex ((Ex (a,A,G)),B,G)) '<' All (('not' (All (a,B,G))),A,G) by BVFUNC_2:19; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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)
let a be Function of Y,BOOLEAN; ::_thesis: 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)
let G be Subset of (PARTITIONS Y); ::_thesis: 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)
let A, B be a_partition of Y; ::_thesis: 'not' (Ex ((Ex (a,A,G)),B,G)) '<' Ex (('not' (Ex (a,B,G))),A,G)
( 'not' (Ex ((Ex (a,A,G)),B,G)) '<' 'not' (All ((Ex (a,B,G)),A,G)) & Ex (('not' (Ex (a,B,G))),A,G) = Ex ((All (('not' a),B,G)),A,G) ) by Th34, BVFUNC_2:19;
hence 'not' (Ex ((Ex (a,A,G)),B,G)) '<' Ex (('not' (Ex (a,B,G))),A,G) by Th19; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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)
let a be Function of Y,BOOLEAN; ::_thesis: 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)
let G be Subset of (PARTITIONS Y); ::_thesis: 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)
let A, B be a_partition of Y; ::_thesis: ( G is independent implies 'not' (Ex ((Ex (a,A,G)),B,G)) = All (('not' (Ex (a,B,G))),A,G) )
assume G is independent ; ::_thesis: 'not' (Ex ((Ex (a,A,G)),B,G)) = All (('not' (Ex (a,B,G))),A,G)
then 'not' (Ex ((Ex (a,A,G)),B,G)) = 'not' (Ex ((Ex (a,B,G)),A,G)) by PARTIT_2:16;
hence 'not' (Ex ((Ex (a,A,G)),B,G)) = All (('not' (Ex (a,B,G))),A,G) by BVFUNC_2:19; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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)
let a be Function of Y,BOOLEAN; ::_thesis: 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)
let G be Subset of (PARTITIONS Y); ::_thesis: 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)
let A, B be a_partition of Y; ::_thesis: ( G is independent implies 'not' (All ((Ex (a,A,G)),B,G)) '<' Ex ((Ex (('not' a),B,G)),A,G) )
assume G is independent ; ::_thesis: 'not' (All ((Ex (a,A,G)),B,G)) '<' Ex ((Ex (('not' a),B,G)),A,G)
then 'not' (All ((Ex (a,A,G)),B,G)) '<' Ex (('not' (All (a,B,G))),A,G) by Th39;
hence 'not' (All ((Ex (a,A,G)),B,G)) '<' Ex ((Ex (('not' a),B,G)),A,G) by BVFUNC_2:18; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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)
let a be Function of Y,BOOLEAN; ::_thesis: 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)
let G be Subset of (PARTITIONS Y); ::_thesis: 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)
let A, B be a_partition of Y; ::_thesis: 'not' (Ex ((Ex (a,A,G)),B,G)) '<' Ex ((Ex (('not' a),B,G)),A,G)
'not' (Ex ((Ex (a,A,G)),B,G)) '<' Ex (('not' (All (a,B,G))),A,G) by Th40;
hence 'not' (Ex ((Ex (a,A,G)),B,G)) '<' Ex ((Ex (('not' a),B,G)),A,G) by BVFUNC_2:18; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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)
let a be Function of Y,BOOLEAN; ::_thesis: 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)
let G be Subset of (PARTITIONS Y); ::_thesis: 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)
let A, B be a_partition of Y; ::_thesis: ( G is independent implies 'not' (All ((Ex (a,A,G)),B,G)) '<' All ((Ex (('not' a),B,G)),A,G) )
assume G is independent ; ::_thesis: 'not' (All ((Ex (a,A,G)),B,G)) '<' All ((Ex (('not' a),B,G)),A,G)
then 'not' (All ((Ex (a,A,G)),B,G)) '<' All (('not' (All (a,B,G))),A,G) by Th41;
hence 'not' (All ((Ex (a,A,G)),B,G)) '<' All ((Ex (('not' a),B,G)),A,G) by BVFUNC_2:18; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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)
let a be Function of Y,BOOLEAN; ::_thesis: 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)
let G be Subset of (PARTITIONS Y); ::_thesis: 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)
let A, B be a_partition of Y; ::_thesis: ( G is independent implies 'not' (Ex ((Ex (a,A,G)),B,G)) '<' All ((Ex (('not' a),B,G)),A,G) )
assume G is independent ; ::_thesis: 'not' (Ex ((Ex (a,A,G)),B,G)) '<' All ((Ex (('not' a),B,G)),A,G)
then 'not' (Ex ((Ex (a,A,G)),B,G)) '<' All (('not' (All (a,B,G))),A,G) by Th42;
hence 'not' (Ex ((Ex (a,A,G)),B,G)) '<' All ((Ex (('not' a),B,G)),A,G) by BVFUNC_2:18; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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)
let a be Function of Y,BOOLEAN; ::_thesis: 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)
let G be Subset of (PARTITIONS Y); ::_thesis: 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)
let A, B be a_partition of Y; ::_thesis: 'not' (Ex ((Ex (a,A,G)),B,G)) '<' Ex ((All (('not' a),B,G)),A,G)
'not' (Ex ((Ex (a,A,G)),B,G)) '<' Ex (('not' (Ex (a,B,G))),A,G) by Th43;
hence 'not' (Ex ((Ex (a,A,G)),B,G)) '<' Ex ((All (('not' a),B,G)),A,G) by BVFUNC_2:19; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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)
let a be Function of Y,BOOLEAN; ::_thesis: 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)
let G be Subset of (PARTITIONS Y); ::_thesis: 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)
let A, B be a_partition of Y; ::_thesis: ( G is independent implies 'not' (Ex ((Ex (a,A,G)),B,G)) = All ((All (('not' a),B,G)),A,G) )
assume G is independent ; ::_thesis: 'not' (Ex ((Ex (a,A,G)),B,G)) = All ((All (('not' a),B,G)),A,G)
then 'not' (Ex ((Ex (a,A,G)),B,G)) = All (('not' (Ex (a,B,G))),A,G) by Th44;
hence 'not' (Ex ((Ex (a,A,G)),B,G)) = All ((All (('not' a),B,G)),A,G) by BVFUNC_2:19; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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))
let a be Function of Y,BOOLEAN; ::_thesis: 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))
let G be Subset of (PARTITIONS Y); ::_thesis: 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))
let A, B be a_partition of Y; ::_thesis: ( G is independent implies Ex (('not' (Ex (a,A,G))),B,G) '<' 'not' (Ex ((All (a,B,G)),A,G)) )
assume G is independent ; ::_thesis: Ex (('not' (Ex (a,A,G))),B,G) '<' 'not' (Ex ((All (a,B,G)),A,G))
then A1: 'not' (All ((Ex (a,A,G)),B,G)) '<' 'not' (Ex ((All (a,B,G)),A,G)) by PARTIT_2:11, PARTIT_2:17;
'not' (All ((Ex (a,A,G)),B,G)) = Ex ((All (('not' a),A,G)),B,G) by Th19;
hence Ex (('not' (Ex (a,A,G))),B,G) '<' 'not' (Ex ((All (a,B,G)),A,G)) by A1, BVFUNC_2:19; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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))
let a be Function of Y,BOOLEAN; ::_thesis: 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))
let G be Subset of (PARTITIONS Y); ::_thesis: 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))
let A, B be a_partition of Y; ::_thesis: All (('not' (Ex (a,A,G))),B,G) '<' 'not' (Ex ((All (a,B,G)),A,G))
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (All (('not' (Ex (a,A,G))),B,G)) . z = TRUE or ('not' (Ex ((All (a,B,G)),A,G))) . z = TRUE )
A1: ( All (('not' (Ex (a,A,G))),B,G) = B_INF (('not' (Ex (a,A,G))),(CompF (B,G))) & z in EqClass (z,(CompF (B,G))) ) by BVFUNC_2:def_9, EQREL_1:def_6;
assume (All (('not' (Ex (a,A,G))),B,G)) . z = TRUE ; ::_thesis: ('not' (Ex ((All (a,B,G)),A,G))) . z = TRUE
then ('not' (Ex (a,A,G))) . z = TRUE by A1, BVFUNC_1:def_16;
then A2: ( Ex (a,A,G) = B_SUP (a,(CompF (A,G))) & 'not' ((Ex (a,A,G)) . z) = TRUE ) by BVFUNC_2:def_10, MARGREL1:def_19;
A3: All (a,B,G) = B_INF (a,(CompF (B,G))) by BVFUNC_2:def_9;
for x being Element of Y st x in EqClass (z,(CompF (A,G))) holds
(All (a,B,G)) . x <> TRUE
proof
let x be Element of Y; ::_thesis: ( x in EqClass (z,(CompF (A,G))) implies (All (a,B,G)) . x <> TRUE )
assume x in EqClass (z,(CompF (A,G))) ; ::_thesis: (All (a,B,G)) . x <> TRUE
then A4: a . x <> TRUE by A2, BVFUNC_1:def_17;
x in EqClass (x,(CompF (B,G))) by EQREL_1:def_6;
hence (All (a,B,G)) . x <> TRUE by A3, A4, BVFUNC_1:def_16; ::_thesis: verum
end;
then ( Ex ((All (a,B,G)),A,G) = B_SUP ((All (a,B,G)),(CompF (A,G))) & (B_SUP ((All (a,B,G)),(CompF (A,G)))) . z = FALSE ) by BVFUNC_1:def_17, BVFUNC_2:def_10;
then 'not' ((Ex ((All (a,B,G)),A,G)) . z) = TRUE ;
hence ('not' (Ex ((All (a,B,G)),A,G))) . z = TRUE by MARGREL1:def_19; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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))
let a be Function of Y,BOOLEAN; ::_thesis: 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))
let G be Subset of (PARTITIONS Y); ::_thesis: 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))
let A, B be a_partition of Y; ::_thesis: All (('not' (Ex (a,A,G))),B,G) '<' 'not' (All ((Ex (a,B,G)),A,G))
'not' (Ex ((Ex (a,A,G)),B,G)) = All (('not' (Ex (a,A,G))),B,G) by BVFUNC_2:19;
hence All (('not' (Ex (a,A,G))),B,G) '<' 'not' (All ((Ex (a,B,G)),A,G)) by Th34; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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))
let a be Function of Y,BOOLEAN; ::_thesis: 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))
let G be Subset of (PARTITIONS Y); ::_thesis: 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))
let A, B be a_partition of Y; ::_thesis: ( G is independent implies All (('not' (Ex (a,A,G))),B,G) = 'not' (Ex ((Ex (a,B,G)),A,G)) )
A1: 'not' (Ex ((Ex (a,A,G)),B,G)) = All (('not' (Ex (a,A,G))),B,G) by BVFUNC_2:19;
assume G is independent ; ::_thesis: All (('not' (Ex (a,A,G))),B,G) = 'not' (Ex ((Ex (a,B,G)),A,G))
hence All (('not' (Ex (a,A,G))),B,G) = 'not' (Ex ((Ex (a,B,G)),A,G)) by A1, PARTIT_2:16; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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)
let a be Function of Y,BOOLEAN; ::_thesis: 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)
let G be Subset of (PARTITIONS Y); ::_thesis: 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)
let A, B be a_partition of Y; ::_thesis: ( G is independent implies Ex (('not' (All (a,A,G))),B,G) = Ex (('not' (All (a,B,G))),A,G) )
A1: 'not' (All ((All (a,A,G)),B,G)) = Ex (('not' (All (a,A,G))),B,G) by BVFUNC_2:18;
assume G is independent ; ::_thesis: Ex (('not' (All (a,A,G))),B,G) = Ex (('not' (All (a,B,G))),A,G)
hence Ex (('not' (All (a,A,G))),B,G) = Ex (('not' (All (a,B,G))),A,G) by A1, Th15; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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)
let a be Function of Y,BOOLEAN; ::_thesis: 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)
let G be Subset of (PARTITIONS Y); ::_thesis: 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)
let A, B be a_partition of Y; ::_thesis: ( G is independent implies All (('not' (All (a,A,G))),B,G) '<' Ex (('not' (All (a,B,G))),A,G) )
A1: 'not' (Ex ((All (a,A,G)),B,G)) = All (('not' (All (a,A,G))),B,G) by BVFUNC_2:19;
assume G is independent ; ::_thesis: All (('not' (All (a,A,G))),B,G) '<' Ex (('not' (All (a,B,G))),A,G)
hence All (('not' (All (a,A,G))),B,G) '<' Ex (('not' (All (a,B,G))),A,G) by A1, Th38; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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)
let a be Function of Y,BOOLEAN; ::_thesis: 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)
let G be Subset of (PARTITIONS Y); ::_thesis: 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)
let A, B be a_partition of Y; ::_thesis: ( G is independent implies Ex (('not' (Ex (a,A,G))),B,G) '<' Ex (('not' (All (a,B,G))),A,G) )
A1: ( 'not' (All ((Ex (a,A,G)),B,G)) = Ex ((All (('not' a),A,G)),B,G) & Ex (('not' (Ex (a,A,G))),B,G) = Ex ((All (('not' a),A,G)),B,G) ) by Th19, BVFUNC_2:19;
assume G is independent ; ::_thesis: Ex (('not' (Ex (a,A,G))),B,G) '<' Ex (('not' (All (a,B,G))),A,G)
hence Ex (('not' (Ex (a,A,G))),B,G) '<' Ex (('not' (All (a,B,G))),A,G) by A1, Th39; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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)
let a be Function of Y,BOOLEAN; ::_thesis: 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)
let G be Subset of (PARTITIONS Y); ::_thesis: 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)
let A, B be a_partition of Y; ::_thesis: All (('not' (Ex (a,A,G))),B,G) '<' Ex (('not' (All (a,B,G))),A,G)
'not' (Ex ((Ex (a,A,G)),B,G)) = All (('not' (Ex (a,A,G))),B,G) by BVFUNC_2:19;
hence All (('not' (Ex (a,A,G))),B,G) '<' Ex (('not' (All (a,B,G))),A,G) by Th40; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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)
let a be Function of Y,BOOLEAN; ::_thesis: 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)
let G be Subset of (PARTITIONS Y); ::_thesis: 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)
let A, B be a_partition of Y; ::_thesis: ( G is independent implies Ex (('not' (Ex (a,A,G))),B,G) '<' All (('not' (All (a,B,G))),A,G) )
A1: ( 'not' (All ((Ex (a,A,G)),B,G)) = Ex ((All (('not' a),A,G)),B,G) & Ex (('not' (Ex (a,A,G))),B,G) = Ex ((All (('not' a),A,G)),B,G) ) by Th19, BVFUNC_2:19;
assume G is independent ; ::_thesis: Ex (('not' (Ex (a,A,G))),B,G) '<' All (('not' (All (a,B,G))),A,G)
hence Ex (('not' (Ex (a,A,G))),B,G) '<' All (('not' (All (a,B,G))),A,G) by A1, Th41; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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)
let a be Function of Y,BOOLEAN; ::_thesis: 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)
let G be Subset of (PARTITIONS Y); ::_thesis: 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)
let A, B be a_partition of Y; ::_thesis: ( G is independent implies All (('not' (Ex (a,A,G))),B,G) '<' All (('not' (All (a,B,G))),A,G) )
assume G is independent ; ::_thesis: All (('not' (Ex (a,A,G))),B,G) '<' All (('not' (All (a,B,G))),A,G)
then 'not' (Ex ((Ex (a,A,G)),B,G)) '<' All (('not' (All (a,B,G))),A,G) by Th42;
hence All (('not' (Ex (a,A,G))),B,G) '<' All (('not' (All (a,B,G))),A,G) by BVFUNC_2:19; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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)
let a be Function of Y,BOOLEAN; ::_thesis: 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)
let G be Subset of (PARTITIONS Y); ::_thesis: 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)
let A, B be a_partition of Y; ::_thesis: All (('not' (Ex (a,A,G))),B,G) '<' Ex (('not' (Ex (a,B,G))),A,G)
'not' (Ex ((Ex (a,A,G)),B,G)) = All (('not' (Ex (a,A,G))),B,G) by BVFUNC_2:19;
hence All (('not' (Ex (a,A,G))),B,G) '<' Ex (('not' (Ex (a,B,G))),A,G) by Th43; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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)
let a be Function of Y,BOOLEAN; ::_thesis: 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)
let G be Subset of (PARTITIONS Y); ::_thesis: 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)
let A, B be a_partition of Y; ::_thesis: ( G is independent implies All (('not' (Ex (a,A,G))),B,G) = All (('not' (Ex (a,B,G))),A,G) )
A1: 'not' (Ex ((Ex (a,A,G)),B,G)) = All (('not' (Ex (a,A,G))),B,G) by BVFUNC_2:19;
assume G is independent ; ::_thesis: All (('not' (Ex (a,A,G))),B,G) = All (('not' (Ex (a,B,G))),A,G)
hence All (('not' (Ex (a,A,G))),B,G) = All (('not' (Ex (a,B,G))),A,G) by A1, Th44; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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)
let a be Function of Y,BOOLEAN; ::_thesis: 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)
let G be Subset of (PARTITIONS Y); ::_thesis: 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)
let A, B be a_partition of Y; ::_thesis: ( G is independent implies Ex (('not' (Ex (a,A,G))),B,G) '<' Ex ((Ex (('not' a),B,G)),A,G) )
A1: ( 'not' (All ((Ex (a,A,G)),B,G)) = Ex ((All (('not' a),A,G)),B,G) & Ex (('not' (Ex (a,A,G))),B,G) = Ex ((All (('not' a),A,G)),B,G) ) by Th19, BVFUNC_2:19;
assume G is independent ; ::_thesis: Ex (('not' (Ex (a,A,G))),B,G) '<' Ex ((Ex (('not' a),B,G)),A,G)
hence Ex (('not' (Ex (a,A,G))),B,G) '<' Ex ((Ex (('not' a),B,G)),A,G) by A1, Th45; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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)
let a be Function of Y,BOOLEAN; ::_thesis: 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)
let G be Subset of (PARTITIONS Y); ::_thesis: 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)
let A, B be a_partition of Y; ::_thesis: All (('not' (Ex (a,A,G))),B,G) '<' Ex ((Ex (('not' a),B,G)),A,G)
'not' (Ex ((Ex (a,A,G)),B,G)) = All (('not' (Ex (a,A,G))),B,G) by BVFUNC_2:19;
hence All (('not' (Ex (a,A,G))),B,G) '<' Ex ((Ex (('not' a),B,G)),A,G) by Th46; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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)
let a be Function of Y,BOOLEAN; ::_thesis: 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)
let G be Subset of (PARTITIONS Y); ::_thesis: 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)
let A, B be a_partition of Y; ::_thesis: ( G is independent implies Ex (('not' (Ex (a,A,G))),B,G) '<' All ((Ex (('not' a),B,G)),A,G) )
A1: ( 'not' (All ((Ex (a,A,G)),B,G)) = Ex ((All (('not' a),A,G)),B,G) & Ex (('not' (Ex (a,A,G))),B,G) = Ex ((All (('not' a),A,G)),B,G) ) by Th19, BVFUNC_2:19;
assume G is independent ; ::_thesis: Ex (('not' (Ex (a,A,G))),B,G) '<' All ((Ex (('not' a),B,G)),A,G)
hence Ex (('not' (Ex (a,A,G))),B,G) '<' All ((Ex (('not' a),B,G)),A,G) by A1, Th47; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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)
let a be Function of Y,BOOLEAN; ::_thesis: 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)
let G be Subset of (PARTITIONS Y); ::_thesis: 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)
let A, B be a_partition of Y; ::_thesis: ( G is independent implies All (('not' (Ex (a,A,G))),B,G) '<' All ((Ex (('not' a),B,G)),A,G) )
A1: 'not' (Ex ((Ex (a,A,G)),B,G)) = All (('not' (Ex (a,A,G))),B,G) by BVFUNC_2:19;
assume G is independent ; ::_thesis: All (('not' (Ex (a,A,G))),B,G) '<' All ((Ex (('not' a),B,G)),A,G)
hence All (('not' (Ex (a,A,G))),B,G) '<' All ((Ex (('not' a),B,G)),A,G) by A1, Th48; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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)
let a be Function of Y,BOOLEAN; ::_thesis: 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)
let G be Subset of (PARTITIONS Y); ::_thesis: 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)
let A, B be a_partition of Y; ::_thesis: All (('not' (Ex (a,A,G))),B,G) '<' Ex ((All (('not' a),B,G)),A,G)
'not' (Ex ((Ex (a,A,G)),B,G)) = All (('not' (Ex (a,A,G))),B,G) by BVFUNC_2:19;
hence All (('not' (Ex (a,A,G))),B,G) '<' Ex ((All (('not' a),B,G)),A,G) by Th49; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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)
let a be Function of Y,BOOLEAN; ::_thesis: 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)
let G be Subset of (PARTITIONS Y); ::_thesis: 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)
let A, B be a_partition of Y; ::_thesis: ( G is independent implies All (('not' (Ex (a,A,G))),B,G) = All ((All (('not' a),B,G)),A,G) )
A1: 'not' (Ex ((Ex (a,A,G)),B,G)) = All (('not' (Ex (a,A,G))),B,G) by BVFUNC_2:19;
assume G is independent ; ::_thesis: All (('not' (Ex (a,A,G))),B,G) = All ((All (('not' a),B,G)),A,G)
hence All (('not' (Ex (a,A,G))),B,G) = All ((All (('not' a),B,G)),A,G) by A1, Th50; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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))
let a be Function of Y,BOOLEAN; ::_thesis: 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))
let G be Subset of (PARTITIONS Y); ::_thesis: 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))
let A, B be a_partition of Y; ::_thesis: ( G is independent implies Ex ((All (('not' a),A,G)),B,G) '<' 'not' (Ex ((All (a,B,G)),A,G)) )
A1: 'not' (All ((Ex (a,A,G)),B,G)) = Ex ((All (('not' a),A,G)),B,G) by Th19;
assume G is independent ; ::_thesis: Ex ((All (('not' a),A,G)),B,G) '<' 'not' (Ex ((All (a,B,G)),A,G))
hence Ex ((All (('not' a),A,G)),B,G) '<' 'not' (Ex ((All (a,B,G)),A,G)) by A1, PARTIT_2:11, PARTIT_2:17; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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))
let a be Function of Y,BOOLEAN; ::_thesis: 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))
let G be Subset of (PARTITIONS Y); ::_thesis: 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))
let A, B be a_partition of Y; ::_thesis: ( G is independent implies All ((All (('not' a),A,G)),B,G) '<' 'not' (Ex ((All (a,B,G)),A,G)) )
A1: ( 'not' (Ex ((Ex (a,A,G)),B,G)) = All (('not' (Ex (a,A,G))),B,G) & All (('not' (Ex (a,A,G))),B,G) = All ((All (('not' a),A,G)),B,G) ) by BVFUNC_2:19;
assume G is independent ; ::_thesis: All ((All (('not' a),A,G)),B,G) '<' 'not' (Ex ((All (a,B,G)),A,G))
hence All ((All (('not' a),A,G)),B,G) '<' 'not' (Ex ((All (a,B,G)),A,G)) by A1, Th33; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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))
let a be Function of Y,BOOLEAN; ::_thesis: 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))
let G be Subset of (PARTITIONS Y); ::_thesis: 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))
let A, B be a_partition of Y; ::_thesis: All ((All (('not' a),A,G)),B,G) '<' 'not' (All ((Ex (a,B,G)),A,G))
( 'not' (Ex ((Ex (a,A,G)),B,G)) = All (('not' (Ex (a,A,G))),B,G) & All (('not' (Ex (a,A,G))),B,G) = All ((All (('not' a),A,G)),B,G) ) by BVFUNC_2:19;
hence All ((All (('not' a),A,G)),B,G) '<' 'not' (All ((Ex (a,B,G)),A,G)) by Th34; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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))
let a be Function of Y,BOOLEAN; ::_thesis: 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))
let G be Subset of (PARTITIONS Y); ::_thesis: 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))
let A, B be a_partition of Y; ::_thesis: ( G is independent implies All ((All (('not' a),A,G)),B,G) '<' 'not' (Ex ((Ex (a,B,G)),A,G)) )
A1: ( 'not' (Ex ((Ex (a,A,G)),B,G)) = All (('not' (Ex (a,A,G))),B,G) & All (('not' (Ex (a,A,G))),B,G) = All ((All (('not' a),A,G)),B,G) ) by BVFUNC_2:19;
assume G is independent ; ::_thesis: All ((All (('not' a),A,G)),B,G) '<' 'not' (Ex ((Ex (a,B,G)),A,G))
hence All ((All (('not' a),A,G)),B,G) '<' 'not' (Ex ((Ex (a,B,G)),A,G)) by A1, PARTIT_2:16; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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)
let a be Function of Y,BOOLEAN; ::_thesis: 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)
let G be Subset of (PARTITIONS Y); ::_thesis: 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)
let A, B be a_partition of Y; ::_thesis: ( G is independent implies Ex ((Ex (('not' a),A,G)),B,G) '<' Ex (('not' (All (a,B,G))),A,G) )
A1: 'not' (All ((All (a,A,G)),B,G)) = Ex ((Ex (('not' a),A,G)),B,G) by Th21;
assume G is independent ; ::_thesis: Ex ((Ex (('not' a),A,G)),B,G) '<' Ex (('not' (All (a,B,G))),A,G)
hence Ex ((Ex (('not' a),A,G)),B,G) '<' Ex (('not' (All (a,B,G))),A,G) by A1, Th15; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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)
let a be Function of Y,BOOLEAN; ::_thesis: 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)
let G be Subset of (PARTITIONS Y); ::_thesis: 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)
let A, B be a_partition of Y; ::_thesis: ( G is independent implies All ((Ex (('not' a),A,G)),B,G) '<' Ex (('not' (All (a,B,G))),A,G) )
A1: 'not' (Ex ((All (a,A,G)),B,G)) = All ((Ex (('not' a),A,G)),B,G) by Th20;
assume G is independent ; ::_thesis: All ((Ex (('not' a),A,G)),B,G) '<' Ex (('not' (All (a,B,G))),A,G)
hence All ((Ex (('not' a),A,G)),B,G) '<' Ex (('not' (All (a,B,G))),A,G) by A1, Th38; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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)
let a be Function of Y,BOOLEAN; ::_thesis: 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)
let G be Subset of (PARTITIONS Y); ::_thesis: 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)
let A, B be a_partition of Y; ::_thesis: ( G is independent implies Ex ((All (('not' a),A,G)),B,G) '<' Ex (('not' (All (a,B,G))),A,G) )
A1: 'not' (All ((Ex (a,A,G)),B,G)) = Ex ((All (('not' a),A,G)),B,G) by Th19;
assume G is independent ; ::_thesis: Ex ((All (('not' a),A,G)),B,G) '<' Ex (('not' (All (a,B,G))),A,G)
hence Ex ((All (('not' a),A,G)),B,G) '<' Ex (('not' (All (a,B,G))),A,G) by A1, Th39; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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)
let a be Function of Y,BOOLEAN; ::_thesis: 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)
let G be Subset of (PARTITIONS Y); ::_thesis: 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)
let A, B be a_partition of Y; ::_thesis: All ((All (('not' a),A,G)),B,G) '<' Ex (('not' (All (a,B,G))),A,G)
( 'not' (Ex ((Ex (a,A,G)),B,G)) = All (('not' (Ex (a,A,G))),B,G) & All (('not' (Ex (a,A,G))),B,G) = All ((All (('not' a),A,G)),B,G) ) by BVFUNC_2:19;
hence All ((All (('not' a),A,G)),B,G) '<' Ex (('not' (All (a,B,G))),A,G) by Th40; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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)
let a be Function of Y,BOOLEAN; ::_thesis: 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)
let G be Subset of (PARTITIONS Y); ::_thesis: 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)
let A, B be a_partition of Y; ::_thesis: ( G is independent implies Ex ((All (('not' a),A,G)),B,G) '<' All (('not' (All (a,B,G))),A,G) )
A1: 'not' (All ((Ex (a,A,G)),B,G)) = Ex ((All (('not' a),A,G)),B,G) by Th19;
assume G is independent ; ::_thesis: Ex ((All (('not' a),A,G)),B,G) '<' All (('not' (All (a,B,G))),A,G)
hence Ex ((All (('not' a),A,G)),B,G) '<' All (('not' (All (a,B,G))),A,G) by A1, Th41; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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)
let a be Function of Y,BOOLEAN; ::_thesis: 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)
let G be Subset of (PARTITIONS Y); ::_thesis: 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)
let A, B be a_partition of Y; ::_thesis: ( G is independent implies All ((All (('not' a),A,G)),B,G) '<' All (('not' (All (a,B,G))),A,G) )
A1: ( 'not' (Ex ((Ex (a,A,G)),B,G)) = All (('not' (Ex (a,A,G))),B,G) & All (('not' (Ex (a,A,G))),B,G) = All ((All (('not' a),A,G)),B,G) ) by BVFUNC_2:19;
assume G is independent ; ::_thesis: All ((All (('not' a),A,G)),B,G) '<' All (('not' (All (a,B,G))),A,G)
hence All ((All (('not' a),A,G)),B,G) '<' All (('not' (All (a,B,G))),A,G) by A1, Th42; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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)
let a be Function of Y,BOOLEAN; ::_thesis: 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)
let G be Subset of (PARTITIONS Y); ::_thesis: 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)
let A, B be a_partition of Y; ::_thesis: All ((All (('not' a),A,G)),B,G) '<' Ex (('not' (Ex (a,B,G))),A,G)
( 'not' (Ex ((Ex (a,A,G)),B,G)) = All (('not' (Ex (a,A,G))),B,G) & All (('not' (Ex (a,A,G))),B,G) = All ((All (('not' a),A,G)),B,G) ) by BVFUNC_2:19;
hence All ((All (('not' a),A,G)),B,G) '<' Ex (('not' (Ex (a,B,G))),A,G) by Th43; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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)
let a be Function of Y,BOOLEAN; ::_thesis: 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)
let G be Subset of (PARTITIONS Y); ::_thesis: 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)
let A, B be a_partition of Y; ::_thesis: ( G is independent implies All ((All (('not' a),A,G)),B,G) = All (('not' (Ex (a,B,G))),A,G) )
assume G is independent ; ::_thesis: All ((All (('not' a),A,G)),B,G) = All (('not' (Ex (a,B,G))),A,G)
then All ((All (('not' a),A,G)),B,G) = All ((All (('not' a),B,G)),A,G) by PARTIT_2:15;
hence All ((All (('not' a),A,G)),B,G) = All (('not' (Ex (a,B,G))),A,G) by BVFUNC_2:19; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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)
let a be Function of Y,BOOLEAN; ::_thesis: 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)
let G be Subset of (PARTITIONS Y); ::_thesis: 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)
let A, B be a_partition of Y; ::_thesis: All ((Ex (('not' a),A,G)),B,G) '<' Ex ((Ex (('not' a),B,G)),A,G)
'not' (Ex ((All (a,A,G)),B,G)) = All ((Ex (('not' a),A,G)),B,G) by Th20;
hence All ((Ex (('not' a),A,G)),B,G) '<' Ex ((Ex (('not' a),B,G)),A,G) by Th13; ::_thesis: verum
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
let Y be non empty set ; ::_thesis: 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)
let a be Function of Y,BOOLEAN; ::_thesis: 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)
let G be Subset of (PARTITIONS Y); ::_thesis: 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)
let A, B be a_partition of Y; ::_thesis: ( G is independent implies Ex ((All (('not' a),A,G)),B,G) '<' Ex ((Ex (('not' a),B,G)),A,G) )
A1: 'not' (All ((Ex (a,A,G)),B,G)) = Ex ((All (('not' a),A,G)),B,G) by Th19;
assume G is independent ; ::_thesis: Ex ((All (('not' a),A,G)),B,G) '<' Ex ((Ex (('not' a),B,G)),A,G)
hence Ex ((All (('not' a),A,G)),B,G) '<' Ex ((Ex (('not' a),B,G)),A,G) by A1, Th45; ::_thesis: verum
end;