let X be finite set ; for M, F being Dependency-set of X st M is (M1) & M is (M2) & M is (M3) & F = { [A,B] where A, B is Subset of X : ex A9, B9 being Subset of X st
( [A9,B9] >= [A,B] & [A9,B9] in M ) } holds
( M = Maximal_wrt F & F is full_family & ( for G being Full-family of X st M = Maximal_wrt G holds
G = F ) )
let M, F be Dependency-set of X; ( M is (M1) & M is (M2) & M is (M3) & F = { [A,B] where A, B is Subset of X : ex A9, B9 being Subset of X st
( [A9,B9] >= [A,B] & [A9,B9] in M ) } implies ( M = Maximal_wrt F & F is full_family & ( for G being Full-family of X st M = Maximal_wrt G holds
G = F ) ) )
assume that
A1:
( M is (M1) & M is (M2) & M is (M3) )
and
A2:
F = { [A,B] where A, B is Subset of X : ex A9, B9 being Subset of X st
( [A9,B9] >= [A,B] & [A9,B9] in M ) }
; ( M = Maximal_wrt F & F is full_family & ( for G being Full-family of X st M = Maximal_wrt G holds
G = F ) )
A3:
F is (F1)
A4:
now for x being set st x in F holds
ex a, b, a9, b9 being Subset of X st
( x = [a,b] & [a9,b9] >= [a,b] & [a9,b9] in M )let x be
set ;
( x in F implies ex a, b, a9, b9 being Subset of X st
( x = [a,b] & [a9,b9] >= [a,b] & [a9,b9] in M ) )assume
x in F
;
ex a, b, a9, b9 being Subset of X st
( x = [a,b] & [a9,b9] >= [a,b] & [a9,b9] in M )then consider a,
b being
Subset of
X such that A5:
x = [a,b]
and A6:
ex
a9,
b9 being
Subset of
X st
(
[a9,b9] >= [a,b] &
[a9,b9] in M )
by A2;
consider a9,
b9 being
Subset of
X such that A7:
[a9,b9] >= [a,b]
and A8:
[a9,b9] in M
by A6;
take a =
a;
ex b, a9, b9 being Subset of X st
( x = [a,b] & [a9,b9] >= [a,b] & [a9,b9] in M )take b =
b;
ex a9, b9 being Subset of X st
( x = [a,b] & [a9,b9] >= [a,b] & [a9,b9] in M )take a9 =
a9;
ex b9 being Subset of X st
( x = [a,b] & [a9,b9] >= [a,b] & [a9,b9] in M )take b9 =
b9;
( x = [a,b] & [a9,b9] >= [a,b] & [a9,b9] in M )thus
(
x = [a,b] &
[a9,b9] >= [a,b] &
[a9,b9] in M )
by A5, A7, A8;
verum end;
A9:
now for A, B being Subset of X st [A,B] in F holds
ex a9, b9 being Subset of X st
( [a9,b9] >= [A,B] & [a9,b9] in M )let A,
B be
Subset of
X;
( [A,B] in F implies ex a9, b9 being Subset of X st
( [a9,b9] >= [A,B] & [a9,b9] in M ) )assume
[A,B] in F
;
ex a9, b9 being Subset of X st
( [a9,b9] >= [A,B] & [a9,b9] in M )then consider a,
b,
a9,
b9 being
Subset of
X such that A10:
[A,B] = [a,b]
and A11:
[a9,b9] >= [a,b]
and A12:
[a9,b9] in M
by A4;
take a9 =
a9;
ex b9 being Subset of X st
( [a9,b9] >= [A,B] & [a9,b9] in M )take b9 =
b9;
( [a9,b9] >= [A,B] & [a9,b9] in M )thus
(
[a9,b9] >= [A,B] &
[a9,b9] in M )
by A10, A11, A12;
verum end;
now for A, B, C being Subset of X st [A,B] in F & [B,C] in F holds
[A,C] in Flet A,
B,
C be
Subset of
X;
( [A,B] in F & [B,C] in F implies [A,C] in F )assume that A13:
[A,B] in F
and A14:
[B,C] in F
;
[A,C] in Fconsider A9,
B9 being
Subset of
X such that A15:
[A9,B9] >= [A,B]
and A16:
[A9,B9] in M
by A9, A13;
consider B19,
C9 being
Subset of
X such that A17:
[B19,C9] >= [B,C]
and A18:
[B19,C9] in M
by A9, A14;
A19:
B19 c= B
by A17;
B c= B9
by A15;
then
B19 c= B9
by A19;
then
C9 c= B9
by A1, A16, A18;
then A20:
[A9,B9] >= [A9,C9]
;
A21:
C c= C9
by A17;
A9 c= A
by A15;
then
[A9,C9] >= [A,C]
by A21;
then
[A9,B9] >= [A,C]
by A20, Th12;
hence
[A,C] in F
by A2, A16;
verum end;
then A22:
F is (F2)
by Th18;
A23:
F is (F4)
proof
let A,
B,
A9,
B9 be
Subset of
X;
ARMSTRNG:def 13 ( [A,B] in F & [A9,B9] in F implies [(A \/ A9),(B \/ B9)] in F )
assume that A24:
[A,B] in F
and A25:
[A9,B9] in F
;
[(A \/ A9),(B \/ B9)] in F
consider a1,
b1 being
Subset of
X such that A26:
[a1,b1] >= [A,B]
and A27:
[a1,b1] in M
by A9, A24;
A28:
B c= b1
by A26;
consider a19,
b19 being
Subset of
X such that A29:
[a19,b19] >= [A9,B9]
and A30:
[a19,b19] in M
by A9, A25;
A31:
B9 c= b19
by A29;
consider A99,
B99 being
Subset of
X such that A32:
[A99,B99] >= [(A \/ A9),(A \/ A9)]
and A33:
[A99,B99] in M
by A1;
A34:
A \/ A9 c= B99
by A32;
a19 c= A9
by A29;
then
a19 c= A \/ A9
by XBOOLE_1:10;
then
a19 c= B99
by A34;
then
b19 c= B99
by A1, A33, A30;
then A35:
B9 c= B99
by A31;
a1 c= A
by A26;
then
a1 c= A \/ A9
by XBOOLE_1:10;
then
a1 c= B99
by A34;
then
b1 c= B99
by A1, A33, A27;
then
B c= B99
by A28;
then A36:
B \/ B9 c= B99 \/ B99
by A35, XBOOLE_1:13;
A99 c= A \/ A9
by A32;
then
[A99,B99] >= [(A \/ A9),(B \/ B9)]
by A36;
hence
[(A \/ A9),(B \/ B9)] in F
by A2, A33;
verum
end;
set DOX = Dependencies-Order X;
now for x being object holds
( ( x in M implies x in Maximal_wrt F ) & ( x in Maximal_wrt F implies x in M ) )let x be
object ;
( ( x in M implies x in Maximal_wrt F ) & ( x in Maximal_wrt F implies x in M ) )hereby ( x in Maximal_wrt F implies x in M )
assume A37:
x in M
;
x in Maximal_wrt Fthen consider a,
b being
Subset of
X such that A38:
x = [a,b]
by Th9;
x is_maximal_wrt F,
Dependencies-Order X
proof
thus
x in F
by A2, A37, A38;
WAYBEL_4:def 23 for b1 being set holds
( not b1 in F or b1 = x or not [x,b1] in Dependencies-Order X )
given y being
set such that A39:
y in F
and A40:
y <> x
and A41:
[x,y] in Dependencies-Order X
;
contradiction
consider e,
f being
Dependency of
X such that A42:
[x,y] = [e,f]
and A43:
e <= f
by A41;
A44:
y = f
by A42, XTUPLE_0:1;
consider c,
d,
c9,
d9 being
Subset of
X such that A45:
y = [c,d]
and A46:
[c9,d9] >= [c,d]
and A47:
[c9,d9] in M
by A4, A39;
A48:
x = e
by A42, XTUPLE_0:1;
then A49:
[c9,d9] >= [a,b]
by A38, A43, A44, A45, A46, Th12;
then A50:
d9 = b
by A1, A37, A38, A47;
c9 = a
by A1, A37, A38, A47, A49;
hence
contradiction
by A38, A40, A43, A48, A44, A45, A46, A50, Th11;
verum
end; hence
x in Maximal_wrt F
by Def1;
verum
end; assume A51:
x in Maximal_wrt F
;
x in Mthen A52:
x is_maximal_wrt F,
Dependencies-Order X
by Def1;
assume A53:
not
x in M
;
contradictionconsider a,
b,
a9,
b9 being
Subset of
X such that A54:
x = [a,b]
and A55:
[a9,b9] >= [a,b]
and A56:
[a9,b9] in M
by A4, A51;
A57:
[[a,b],[a9,b9]] in Dependencies-Order X
by A55;
[a9,b9] in F
by A2, A56;
hence
contradiction
by A52, A54, A56, A53, A57;
verum end;
hence
M = Maximal_wrt F
by TARSKI:2; ( F is full_family & ( for G being Full-family of X st M = Maximal_wrt G holds
G = F ) )
F is (F3)
proof
let A,
B,
A9,
B9 be
Subset of
X;
ARMSTRNG:def 12 ( [A,B] in F & [A,B] >= [A9,B9] implies [A9,B9] in F )
assume that A58:
[A,B] in F
and A59:
[A,B] >= [A9,B9]
;
[A9,B9] in F
consider a9,
b9 being
Subset of
X such that A60:
[a9,b9] >= [A,B]
and A61:
[a9,b9] in M
by A9, A58;
[a9,b9] >= [A9,B9]
by A59, A60, Th12;
hence
[A9,B9] in F
by A2, A61;
verum
end;
hence
F is full_family
by A3, A22, A23; for G being Full-family of X st M = Maximal_wrt G holds
G = F
let G be Full-family of X; ( M = Maximal_wrt G implies G = F )
assume A62:
M = Maximal_wrt G
; G = F
now for x being object holds
( ( x in G implies x in F ) & ( x in F implies x in G ) )let x be
object ;
( ( x in G implies x in F ) & ( x in F implies x in G ) )hereby ( x in F implies x in G )
A63:
field (Dependencies-Order X) = [:(bool X),(bool X):]
by Th17;
assume A64:
x in G
;
x in Fthen consider a,
b being
Subset of
X such that A65:
x = [a,b]
by Th9;
defpred S1[
object ]
means ex
y being
Dependency of
X st
( $1
= y &
y >= [a,b] );
consider MA being
set such that A66:
for
x being
object holds
(
x in MA iff (
x in G &
S1[
x] ) )
from XBOOLE_0:sch 1();
MA c= G
by A66;
then A67:
MA is
finite Subset of
(field (Dependencies-Order X))
by A63, XBOOLE_1:1;
MA <> {}
by A64, A65, A66;
then consider m being
Element of
MA such that A68:
m is_maximal_wrt MA,
Dependencies-Order X
by A67, Th2;
A69:
m in MA
by A68;
then
m in G
by A66;
then A70:
ex
a9,
b9 being
Subset of
X st
m = [a9,b9]
by Th9;
m is_maximal_wrt G,
Dependencies-Order X
proof
A71:
ex
mm being
Dependency of
X st
(
m = mm &
mm >= [a,b] )
by A66, A69;
thus
m in G
by A66, A69;
WAYBEL_4:def 23 for b1 being set holds
( not b1 in G or b1 = m or not [m,b1] in Dependencies-Order X )
given y being
set such that A72:
y in G
and A73:
y <> m
and A74:
[m,y] in Dependencies-Order X
;
contradiction
consider e,
f being
Dependency of
X such that A75:
[m,y] = [e,f]
and A76:
e <= f
by A74;
A77:
y = f
by A75, XTUPLE_0:1;
m = e
by A75, XTUPLE_0:1;
then
f >= [a,b]
by A71, A76, Th12;
then
y in MA
by A66, A72, A77;
hence
contradiction
by A68, A73, A74;
verum
end; then A78:
m in (Dependencies-Order X) Maximal_in G
by Def1;
ex
y being
Dependency of
X st
(
m = y &
y >= [a,b] )
by A66, A69;
hence
x in F
by A2, A62, A65, A78, A70;
verum
end; assume
x in F
;
x in Gthen
ex
a,
b,
a1,
b1 being
Subset of
X st
(
x = [a,b] &
[a1,b1] >= [a,b] &
[a1,b1] in M )
by A4;
hence
x in G
by A62, Def12;
verum end;
hence
G = F
by TARSKI:2; verum