let X be set ; :: thesis: for F being Dependency-set of X
for A, B being Subset of holds
( A ^|^ B,F iff ( [A,B] in F & ( for A', B' being Subset of 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 holds
( A ^|^ B,F iff ( [A,B] in F & ( for A', B' being Subset of 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 ; :: thesis: ( x ^|^ y,F iff ( [x,y] in F & ( for A', B' being Subset of 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 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 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;
hence [x,y] in F ; :: thesis: for x', y' being Subset of holds
( not [x',y'] in F or ( not x <> x' & not y <> y' ) or not [x,y] <= [x',y'] )
A2: [x,y] is_maximal_wrt F, Dependencies-Order X by A1, Def1;
given x', y' being Subset of such that A3: [x',y'] in F and
A4: ( x <> x' or y <> y' ) and
A5: [x,y] <= [x',y'] ; :: thesis: contradiction
A6: [[x,y],[x',y']] in Dependencies-Order X by A5;
[x,y] <> [x',y'] by A4, ZFMISC_1:33;
hence contradiction by A2, A3, A6, WAYBEL_4:def 24; :: thesis: verum

end;

assume that
A7: [x,y] in F and
A8: for x', y' being Subset of 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 A7; :: 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 A9: z in F and
A10: z <> [x,y] and
A11: [[x,y],z] in Dependencies-Order X ; :: thesis: contradiction
consider x', y' being set such that
A12: z = [x',y'] and
A13: x' in bool X and
A14: y' in bool X by A9, RELSET_1:6;
consider e, f being Dependency of X such that
A15: [[x,y],z] = [e,f] and
A16: e <= f by A11;
A17: e = [x,y] by A15, ZFMISC_1:33;
A18: f = z by A15, ZFMISC_1:33;
reconsider x' = x', y' = y' as Subset of by A13, A14;
( x <> x' or y <> y' ) by A10, A12;
hence contradiction by A8, A9, A12, A13, A14, A16, A17, A18; :: thesis: verum

end;

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