let X be set ; :: thesis: 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; :: thesis: { [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):]

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { [A,B] where A, B is Subset of X : ( K c= A or B c= A ) } or x in [:(bool X),(bool X):] )
assume x in { [A,B] where A, B is Subset of X : ( K c= A or B c= A ) } ; :: thesis: x in [:(bool X),(bool X):]
then ex A, B being Subset of X st
( x = [A,B] & ( K c= A or B c= A ) ) ;
hence x in [:(bool X),(bool X):] ; :: thesis: verum

end;

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; :: according to ARMSTRNG:def 13 :: thesis: ( [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 ; :: thesis: [(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 ; :: thesis: verum

end;

now :: thesis: for A, B, C being Subset of X st [A,B] in F & [B,C] in F holds
[A,C] in F

let A, B, C be Subset of X; :: thesis: ( [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 ; :: thesis: [A,C] in F
consider 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; :: thesis: 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; :: thesis: verum