let X be set ; :: thesis: for K being Subset of holds { [A,B] where A, B is Subset of : ( K c= A or B c= A ) } is Full-family of X
let K be Subset of ; :: thesis: { [A,B] where A, B is Subset of : ( K c= A or B c= A ) } is Full-family of X
set F = { [A,B] where A, B is Subset of : ( K c= A or B c= A ) } ;
{ [A,B] where A, B is Subset of : ( K c= A or B c= A ) } c= [:(bool X),(bool X):]

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { [A,B] where A, B is Subset of : ( 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 : ( K c= A or B c= A ) } ; :: thesis: x in [:(bool X),(bool X):]
then ex A, B being Subset of 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 : ( K c= A or B c= A ) } as Dependency-set of X ;
A1: F is (F4)

proof

let A, B, A', B' be Subset of ; :: according to ARMSTRNG:def 14 :: thesis: ( [A,B] in F & [A',B'] in F implies [(A \/ A'),(B \/ B')] in F )
assume that
A2: [A,B] in F and
A3: [A',B'] in F ; :: thesis: [(A \/ A'),(B \/ B')] in F
consider a, b being Subset of such that
A4: [A,B] = [a,b] and
A5: ( K c= a or b c= a ) by A2;
A6: B = b by A4, ZFMISC_1:33;
consider a', b' being Subset of such that
A7: [A',B'] = [a',b'] and
A8: ( K c= a' or b' c= a' ) by A3;
A9: A' = a' by A7, ZFMISC_1:33;
A10: B' = b' by A7, ZFMISC_1:33;
A = a by A4, ZFMISC_1:33;
then ( K c= A \/ A' or B \/ B' c= A \/ A' ) by A5, A8, A6, A9, A10, XBOOLE_1:10, XBOOLE_1:13;
hence [(A \/ A'),(B \/ B')] in F ; :: thesis: verum

end;

now

let A, B, C be Subset of ; :: 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 such that
A13: [A,B] = [a,b] and
A14: ( K c= a or b c= a ) by A11;
A15: A = a by A13, ZFMISC_1:33;
consider b1, c being Subset of such that
A16: [B,C] = [b1,c] and
A17: ( K c= b1 or c c= b1 ) by A12;
A18: B = b1 by A16, ZFMISC_1:33;
A19: C = c by A16, ZFMISC_1:33;
B = b by A13, ZFMISC_1:33;
then ( K c= a or c c= a ) by A14, A17, A18, XBOOLE_1:1;
hence [A,C] in F by A15, A19; :: thesis: verum

end;

then A20: F is (F2) by Th20;
F is (DC3)

proof

let A, B be Subset of ; :: according to ARMSTRNG:def 16 :: thesis: ( B c= A implies [A,B] in F )
assume B c= A ; :: thesis: [A,B] in F
hence [A,B] in F ; :: thesis: verum

end;

hence { [A,B] where A, B is Subset of : ( K c= A or B c= A ) } is Full-family of X by A20, A1; :: thesis: verum