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 set ; :: 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 ;
F is full_family

proof

A1: now

let A, B, C be Subset of X; :: thesis: ( [A,B] in F & [B,C] in F implies [A,C] in F )
assume A2: ( [A,B] in F & [B,C] in F ) ; :: thesis: [A,C] in F
then consider a, b being Subset of X such that
A3: [A,B] = [a,b] and
A4: ( K c= a or b c= a ) ;
consider b1, c being Subset of X such that
A5: [B,C] = [b1,c] and
A6: ( K c= b1 or c c= b1 ) by A2;
A7: ( A = a & B = b & B = b1 & C = c ) by A3, A5, ZFMISC_1:33;
then ( K c= a or c c= a ) by A4, A6, XBOOLE_1:1;
hence [A,C] in F by A7; :: thesis: verum

end;

then A8: F is (F2) by Th20;
A9: F is (DC3)

proof

let A, B be Subset of X; :: 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 F is (F1) by A8; :: according to ARMSTRNG:def 15 :: thesis: ( F is (F2) & F is (F3) & F is (F4) )
thus F is (F2) by A1, Th20; :: thesis: ( F is (F3) & F is (F4) )
hence F is (F3) by A9; :: thesis: F is (F4)
thus F is (F4) :: thesis: verum

proof

let A, B, A', B' be Subset of X; :: according to ARMSTRNG:def 14 :: thesis: ( [A,B] in F & [A',B'] in F implies [(A \/ A'),(B \/ B')] in F )
assume A10: ( [A,B] in F & [A',B'] in F ) ; :: thesis: [(A \/ A'),(B \/ B')] in F
then consider a, b being Subset of X such that
A11: ( [A,B] = [a,b] & ( K c= a or b c= a ) ) ;
consider a', b' being Subset of X such that
A12: ( [A',B'] = [a',b'] & ( K c= a' or b' c= a' ) ) by A10;
( A = a & B = b & A' = a' & B' = b' ) by A11, A12, ZFMISC_1:33;
then ( K c= A \/ A' or B \/ B' c= A \/ A' ) by A11, A12, XBOOLE_1:10, XBOOLE_1:13;
hence [(A \/ A'),(B \/ B')] in F ; :: thesis: verum

end;

end;

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