let X be finite set ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in S or a in field (Dependencies-Order X) )
assume a in S ; :: thesis: a in field (Dependencies-Order X)
then ex b being Element of FF st
( a = b & x <= b ) ;
hence a in field (Dependencies-Order X) by A2; :: thesis: verum

end;

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 ; :: thesis: ex B being Subset of X st
( [a,B] in Maximal_wrt F & [a,B] >= x )
take b ; :: thesis: ( [a,b] in Maximal_wrt F & [a,b] >= x )
m is_maximal_wrt F, Dependencies-Order X

proof

thus m in F by A5; :: according to WAYBEL_4:def 23 :: thesis: for b₁ being set holds
( not b₁ in F or b₁ = m or not [m,b₁] 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 ; :: thesis: 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; :: thesis: verum

end;

hence [a,b] in Maximal_wrt F by A6, Def1; :: thesis: [a,b] >= x
thus [a,b] >= x by A5, A6; :: thesis: verum