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

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

assume x ^|^ y,F ; :: thesis: ( [x,y] in F & ( for x9, y9 being Subset of X holds
( not [x9,y9] in F or ( not x <> x9 & not y <> y9 ) or not [x,y] <= [x9,y9] ) ) )
then A1: [x,y] in Maximal_wrt F ;
hence [x,y] in F ; :: thesis: for x9, y9 being Subset of X holds
( not [x9,y9] in F or ( not x <> x9 & not y <> y9 ) or not [x,y] <= [x9,y9] )
A2: [x,y] is_maximal_wrt F, Dependencies-Order X by A1, Def1;
given x9, y9 being Subset of X such that A3: [x9,y9] in F and
A4: ( x <> x9 or y <> y9 ) and
A5: [x,y] <= [x9,y9] ; :: thesis: contradiction
A6: [[x,y],[x9,y9]] in Dependencies-Order X by A5;
[x,y] <> [x9,y9] by A4, XTUPLE_0:1;
hence contradiction by A2, A3, A6; :: thesis: verum

end;

assume that
A7: [x,y] in F and
A8: for x9, y9 being Subset of X holds
( not [x9,y9] in F or ( not x <> x9 & not y <> y9 ) or not [x,y] <= [x9,y9] ) ; :: 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 23 :: 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 x9, y9 being object such that
A12: z = [x9,y9] and
A13: x9 in bool X and
A14: y9 in bool X by A9, RELSET_1:2;
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, XTUPLE_0:1;
A18: f = z by A15, XTUPLE_0:1;
reconsider x9 = x9, y9 = y9 as Subset of X by A13, A14;
( x <> x9 or y <> y9 ) 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 ; :: thesis: verum