let X be set ; 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; 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; ( 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 ( [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
;
( [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
;
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]
;
contradictionA6:
[[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;
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] )
; x ^|^ y,F
[x,y] is_maximal_wrt F, Dependencies-Order X
proof
thus
[x,y] in F
by A7;
WAYBEL_4:def 23 for b1 being set holds
( not b1 in F or b1 = [x,y] or not [[x,y],b1] 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
;
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;
verum
end;
then
[x,y] in Maximal_wrt F
by Def1;
hence
x ^|^ y,F
; verum