let X be non empty finite set ; for F being Full-family of X holds
( Maximal_wrt F is (M1) & Maximal_wrt F is (M2) & Maximal_wrt F is (M3) )
let F be full_family Dependency-set of X; ( Maximal_wrt F is (M1) & Maximal_wrt F is (M2) & Maximal_wrt F is (M3) )
set DOX = Dependencies-Order X;
set MEF = Maximal_wrt F;
thus
Maximal_wrt F is (M1)
( Maximal_wrt F is (M2) & Maximal_wrt F is (M3) )proof
A1:
field (Dependencies-Order X) = [:(bool X),(bool X):]
by Th17;
let A be
Subset of
X;
ARMSTRNG:def 18 ex A9, B9 being Subset of X st
( [A9,B9] >= [A,A] & [A9,B9] in Maximal_wrt F )
defpred S1[
object ]
means ex
y being
Dependency of
X st
( $1
= y &
y >= [A,A] );
consider MA being
set such that A2:
for
x being
object holds
(
x in MA iff (
x in F &
S1[
x] ) )
from XBOOLE_0:sch 1();
MA c= F
by A2;
then A3:
MA is
finite Subset of
(field (Dependencies-Order X))
by A1, XBOOLE_1:1;
[A,A] in F
by Def15;
then
MA <> {}
by A2;
then consider x being
Element of
MA such that A4:
x is_maximal_wrt MA,
Dependencies-Order X
by A3, Th2;
A5:
x in MA
by A4;
then
x in F
by A2;
then consider A9,
B9 being
object such that A6:
A9 in bool X
and A7:
B9 in bool X
and A8:
x = [A9,B9]
by ZFMISC_1:def 2;
reconsider A9 =
A9,
B9 =
B9 as
Subset of
X by A6, A7;
take
A9
;
ex B9 being Subset of X st
( [A9,B9] >= [A,A] & [A9,B9] in Maximal_wrt F )
take
B9
;
( [A9,B9] >= [A,A] & [A9,B9] in Maximal_wrt F )
A9:
ex
y being
Dependency of
X st
(
x = y &
y >= [A,A] )
by A2, A5;
hence
[A9,B9] >= [A,A]
by A8;
[A9,B9] in Maximal_wrt F
x is_maximal_wrt F,
Dependencies-Order X
proof
thus
x in F
by A2, A5;
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 z being
set such that A10:
z in F
and A11:
z <> x
and A12:
[x,z] in Dependencies-Order X
;
contradiction
consider e,
f being
Dependency of
X such that A13:
[x,z] = [e,f]
and A14:
e <= f
by A12;
x = e
by A13, XTUPLE_0:1;
then A15:
f >= [A,A]
by A9, A14, Th12;
z = f
by A13, XTUPLE_0:1;
then
z in MA
by A2, A10, A15;
hence
contradiction
by A4, A11, A12;
verum
end;
hence
[A9,B9] in Maximal_wrt F
by A8, Def1;
verum
end;
thus
Maximal_wrt F is (M2)
Maximal_wrt F is (M3) proof
let A,
B,
A9,
B9 be
Subset of
X;
ARMSTRNG:def 19 ( [A,B] in Maximal_wrt F & [A9,B9] in Maximal_wrt F & [A,B] >= [A9,B9] implies ( A = A9 & B = B9 ) )
assume that A16:
[A,B] in Maximal_wrt F
and A17:
[A9,B9] in Maximal_wrt F
and A18:
[A,B] >= [A9,B9]
;
( A = A9 & B = B9 )
A19:
[[A9,B9],[A,B]] in Dependencies-Order X
by A18;
assume
( not
A = A9 or not
B = B9 )
;
contradiction
then A20:
[A,B] <> [A9,B9]
by XTUPLE_0:1;
[A9,B9] is_maximal_wrt F,
Dependencies-Order X
by A17, Def1;
hence
contradiction
by A16, A20, A19;
verum
end;
thus
Maximal_wrt F is (M3)
verumproof
let A,
B,
A9,
B9 be
Subset of
X;
ARMSTRNG:def 20 ( [A,B] in Maximal_wrt F & [A9,B9] in Maximal_wrt F & A9 c= B implies B9 c= B )
assume that A21:
[A,B] in Maximal_wrt F
and A22:
[A9,B9] in Maximal_wrt F
and A23:
A9 c= B
;
B9 c= B
A24:
A ^|^ B,
F
by A21;
[A9,B9] >= [B,B9]
by A23;
then
[B,B9] in F
by A22, Def12;
then A25:
[A,B9] in F
by A21, Th18;
B c= B \/ B9
by XBOOLE_1:7;
then A26:
[A,(B \/ B9)] >= [A,B]
;
A \/ A = A
;
then
[A,(B \/ B9)] in F
by A21, A25, Def13;
then
B \/ B9 = B
by A24, A26, Th27;
hence
B9 c= B
by XBOOLE_1:11;
verum
end;