let X be finite set ; for P being Dependency of X
for F being Dependency-set of X st P in F holds
ex A, B being Subset of X st
( [A,B] in Maximal_wrt F & [A,B] >= P )
let x be Dependency of X; for F being Dependency-set of X st x in F holds
ex A, B being Subset of X st
( [A,B] in Maximal_wrt F & [A,B] >= x )
let F be Dependency-set of X; ( x in F implies ex A, B being Subset of X st
( [A,B] in Maximal_wrt F & [A,B] >= x ) )
set DOX = Dependencies-Order X;
assume A1:
x in F
; ex A, B being Subset of X st
( [A,B] in Maximal_wrt F & [A,B] >= x )
then reconsider FF = F as non empty Dependency-set of X ;
reconsider S = { y where y is Element of FF : x <= y } as set ;
A2:
field (Dependencies-Order X) = [:(bool X),(bool X):]
by Th17;
A3:
S c= field (Dependencies-Order X)
x in S
by A1;
then consider m being Element of S such that
A4:
m is_maximal_wrt S, Dependencies-Order X
by A3, Th2;
m in S
by A4;
then A5:
ex y being Element of FF st
( m = y & x <= y )
;
then consider a, b being Subset of X such that
A6:
m = [a,b]
by Th8;
take
a
; ex B being Subset of X st
( [a,B] in Maximal_wrt F & [a,B] >= x )
take
b
; ( [a,b] in Maximal_wrt F & [a,b] >= x )
m is_maximal_wrt F, Dependencies-Order X
proof
thus
m in F
by A5;
WAYBEL_4:def 23 for b1 being set holds
( not b1 in F or b1 = m or not [m,b1] in Dependencies-Order X )
given y being
set such that A7:
y in F
and A8:
y <> m
and A9:
[m,y] in Dependencies-Order X
;
contradiction
consider e,
f being
Dependency of
X such that A10:
[m,y] = [e,f]
and A11:
e <= f
by A9;
reconsider y =
y as
Element of
FF by A7;
A12:
y = f
by A10, XTUPLE_0:1;
m = e
by A10, XTUPLE_0:1;
then
x <= y
by A5, A11, A12, Th12;
then
y in S
;
hence
contradiction
by A4, A8, A9;
verum
end;
hence
[a,b] in Maximal_wrt F
by A6, Def1; [a,b] >= x
thus
[a,b] >= x
by A5, A6; verum