let X be set ; for K being Subset of X holds { [A,B] where A, B is Subset of X : ( K c= A or B c= A ) } is Full-family of X
let K be Subset of X; { [A,B] where A, B is Subset of X : ( K c= A or B c= A ) } is Full-family of X
set F = { [A,B] where A, B is Subset of X : ( K c= A or B c= A ) } ;
{ [A,B] where A, B is Subset of X : ( K c= A or B c= A ) } c= [:(bool X),(bool X):]
then reconsider F = { [A,B] where A, B is Subset of X : ( K c= A or B c= A ) } as Dependency-set of X ;
A1:
F is (F4)
proof
let A,
B,
A9,
B9 be
Subset of
X;
ARMSTRNG:def 13 ( [A,B] in F & [A9,B9] in F implies [(A \/ A9),(B \/ B9)] in F )
assume that A2:
[A,B] in F
and A3:
[A9,B9] in F
;
[(A \/ A9),(B \/ B9)] in F
consider a,
b being
Subset of
X such that A4:
[A,B] = [a,b]
and A5:
(
K c= a or
b c= a )
by A2;
A6:
B = b
by A4, XTUPLE_0:1;
consider a9,
b9 being
Subset of
X such that A7:
[A9,B9] = [a9,b9]
and A8:
(
K c= a9 or
b9 c= a9 )
by A3;
A9:
A9 = a9
by A7, XTUPLE_0:1;
A10:
B9 = b9
by A7, XTUPLE_0:1;
A = a
by A4, XTUPLE_0:1;
then
(
K c= A \/ A9 or
B \/ B9 c= A \/ A9 )
by A5, A8, A6, A9, A10, XBOOLE_1:10, XBOOLE_1:13;
hence
[(A \/ A9),(B \/ B9)] in F
;
verum
end;
now for A, B, C being Subset of X st [A,B] in F & [B,C] in F holds
[A,C] in Flet A,
B,
C be
Subset of
X;
( [A,B] in F & [B,C] in F implies [A,C] in F )assume that A11:
[A,B] in F
and A12:
[B,C] in F
;
[A,C] in Fconsider a,
b being
Subset of
X such that A13:
[A,B] = [a,b]
and A14:
(
K c= a or
b c= a )
by A11;
A15:
A = a
by A13, XTUPLE_0:1;
consider b1,
c being
Subset of
X such that A16:
[B,C] = [b1,c]
and A17:
(
K c= b1 or
c c= b1 )
by A12;
A18:
B = b1
by A16, XTUPLE_0:1;
A19:
C = c
by A16, XTUPLE_0:1;
B = b
by A13, XTUPLE_0:1;
then
(
K c= a or
c c= a )
by A14, A17, A18;
hence
[A,C] in F
by A15, A19;
verum end;
then A20:
F is (F2)
by Th18;
F is (DC3)
;
hence
{ [A,B] where A, B is Subset of X : ( K c= A or B c= A ) } is Full-family of X
by A20, A1; verum