let X be set ; :: thesis: for F being Dependency-set of X
for A, B being Subset of X holds
( A ^|^ B,F iff ( [A,B] in F & ( for A', B' being Subset of X holds
( not [A',B'] in F or ( not A <> A' & not B <> B' ) or not [A,B] <= [A',B'] ) ) ) )
let F be Dependency-set of X; :: thesis: for A, B being Subset of X holds
( A ^|^ B,F iff ( [A,B] in F & ( for A', B' being Subset of X holds
( not [A',B'] in F or ( not A <> A' & not B <> B' ) or not [A,B] <= [A',B'] ) ) ) )
let x, y be Subset of X; :: thesis: ( x ^|^ y,F iff ( [x,y] in F & ( for A', B' being Subset of X holds
( not [A',B'] in F or ( not x <> A' & not y <> B' ) or not [x,y] <= [A',B'] ) ) ) )
set DOX = Dependencies-Order X;

hereby :: thesis: ( [x,y] in F & ( for A', B' being Subset of X holds
( not [A',B'] in F or ( not x <> A' & not y <> B' ) or not [x,y] <= [A',B'] ) ) implies x ^|^ y,F )

assume x ^|^ y,F ; :: thesis: ( [x,y] in F & ( for x', y' being Subset of X holds
( not [x',y'] in F or ( not x <> x' & not y <> y' ) or not [x,y] <= [x',y'] ) ) )
then A1: [x,y] in Maximal_wrt F by Def18;
then A2: [x,y] is_maximal_wrt F, Dependencies-Order X by Def1;
thus [x,y] in F by A1; :: thesis: for x', y' being Subset of X holds
( not [x',y'] in F or ( not x <> x' & not y <> y' ) or not [x,y] <= [x',y'] )
given x', y' being Subset of X such that A3: ( [x',y'] in F & ( x <> x' or y <> y' ) & [x,y] <= [x',y'] ) ; :: thesis: contradiction
A4: [x,y] <> [x',y'] by A3, ZFMISC_1:33;
[[x,y],[x',y']] in Dependencies-Order X by A3;
hence contradiction by A2, A3, A4, WAYBEL_4:def 24; :: thesis: verum

end;

assume A5: ( [x,y] in F & ( for x', y' being Subset of X holds
( not [x',y'] in F or ( not x <> x' & not y <> y' ) or not [x,y] <= [x',y'] ) ) ) ; :: thesis: x ^|^ y,F
[x,y] is_maximal_wrt F, Dependencies-Order X

proof

thus [x,y] in F by A5; :: according to WAYBEL_4:def 24 :: thesis: for b₁ being set holds
( not b₁ in F or b₁ = [x,y] or not [[x,y],b₁] in Dependencies-Order X )
given z being set such that A6: ( z in F & z <> [x,y] & [[x,y],z] in Dependencies-Order X ) ; :: thesis: contradiction
consider x', y' being set such that
A7: ( z = [x',y'] & x' in bool X & y' in bool X ) by A6, RELSET_1:6;
reconsider x' = x', y' = y' as Subset of X by A7;
A8: ( x <> x' or y <> y' ) by A6, A7;
consider e, f being Dependency of X such that
A9: ( [[x,y],z] = [e,f] & e <= f ) by A6;
( e = [x,y] & f = z ) by A9, ZFMISC_1:33;
hence contradiction by A5, A6, A7, A8, A9; :: thesis: verum

end;

then [x,y] in Maximal_wrt F by Def1;
hence x ^|^ y,F by Def18; :: thesis: verum