let X be set ; :: thesis: for B being Subset-Family of X
for F being Dependency-set of X holds X deps_encl_by B is full_family
let B be Subset-Family of X; :: thesis: for F being Dependency-set of X holds X deps_encl_by B is full_family
let F be Dependency-set of X; :: thesis: X deps_encl_by B is full_family
set F = X deps_encl_by B;

per cases ( not B is (C1) or B is (C1) ) ;

suppose A1: not B is (C1) ; :: thesis: X deps_encl_by B is full_family

now

let x be set ; :: thesis: ( ( x in X deps_encl_by B implies x in Dependencies X ) & ( x in Dependencies X implies x in X deps_encl_by B ) )
thus ( x in X deps_encl_by B implies x in Dependencies X ) ; :: thesis: ( x in Dependencies X implies x in X deps_encl_by B )
assume x in Dependencies X ; :: thesis: x in X deps_encl_by B
then consider x1, x2 being set such that
A2: ( x1 in bool X & x2 in bool X & x = [x1,x2] ) by ZFMISC_1:def 2;
for g being set st g in B & x1 c= g holds
x2 c= g by A1;
hence x in X deps_encl_by B by A2; :: thesis: verum

end;

then X deps_encl_by B = Dependencies X by TARSKI:2;
then ( X deps_encl_by B is (F1) & X deps_encl_by B is (F2) & X deps_encl_by B is (F3) & X deps_encl_by B is (F4) ) by Th21;
hence X deps_encl_by B is full_family ; :: thesis: verum

end;

suppose B is (C1) ; :: thesis: X deps_encl_by B is full_family

then reconsider B = B as non empty Subset-Family of X ;

A3: now

let x, y be Subset of X; :: thesis: for c being Element of B st [x,y] in X deps_encl_by B & x c= c holds
y c= c
let c be Element of B; :: thesis: ( [x,y] in X deps_encl_by B & x c= c implies y c= c )
assume that
A4: [x,y] in X deps_encl_by B and
A5: x c= c ; :: thesis: y c= c
consider a, b being Subset of X such that
A6: [x,y] = [a,b] and
A7: for c being set st c in B & a c= c holds
b c= c by A4;
( x = a & y = b ) by A6, ZFMISC_1:33;
hence y c= c by A5, A7; :: thesis: verum

end;

thus X deps_encl_by B is (F1) :: according to ARMSTRNG:def 15 :: thesis: ( X deps_encl_by B is (F2) & X deps_encl_by B is (F3) & X deps_encl_by B is (F4) )

proof

let A be Subset of X; :: according to ARMSTRNG:def 12 :: thesis: [A,A] in X deps_encl_by B
for c being set st c in B & A c= c holds
A c= c ;
hence [A,A] in X deps_encl_by B ; :: thesis: verum

end;

now

let a, b, c be Subset of X; :: thesis: ( [a,b] in X deps_encl_by B & [b,c] in X deps_encl_by B implies [a,c] in X deps_encl_by B )
assume that
A8: [a,b] in X deps_encl_by B and
A9: [b,c] in X deps_encl_by B ; :: thesis: [a,c] in X deps_encl_by B

now

let x be set ; :: thesis: ( x in B & a c= x implies c c= x )
assume A10: ( x in B & a c= x ) ; :: thesis: c c= x
then b c= x by A3, A8;
hence c c= x by A3, A9, A10; :: thesis: verum

end;

hence [a,c] in X deps_encl_by B ; :: thesis: verum

end;

hence X deps_encl_by B is (F2) by Th20; :: thesis: ( X deps_encl_by B is (F3) & X deps_encl_by B is (F4) )
thus X deps_encl_by B is (F3) :: thesis: X deps_encl_by B is (F4)

proof

let a, b, a', b' be Subset of X; :: according to ARMSTRNG:def 13 :: thesis: ( [a,b] in X deps_encl_by B & [a,b] >= [a',b'] implies [a',b'] in X deps_encl_by B )
assume that
A11: [a,b] in X deps_encl_by B and
A12: [a,b] >= [a',b'] ; :: thesis: [a',b'] in X deps_encl_by B
A13: ( a c= a' & b' c= b ) by A12, Th15;

now

let c be set ; :: thesis: ( c in B & a' c= c implies b' c= c )
assume A14: ( c in B & a' c= c ) ; :: thesis: b' c= c
then a c= c by A13, XBOOLE_1:1;
then b c= c by A3, A11, A14;
hence b' c= c by A13, XBOOLE_1:1; :: thesis: verum

end;

hence [a',b'] in X deps_encl_by B ; :: thesis: verum

end;

thus X deps_encl_by B is (F4) :: thesis: verum

proof

let a, b, a', b' be Subset of X; :: according to ARMSTRNG:def 14 :: thesis: ( [a,b] in X deps_encl_by B & [a',b'] in X deps_encl_by B implies [(a \/ a'),(b \/ b')] in X deps_encl_by B )
assume that
A15: [a,b] in X deps_encl_by B and
A16: [a',b'] in X deps_encl_by B ; :: thesis: [(a \/ a'),(b \/ b')] in X deps_encl_by B

now

let c be set ; :: thesis: ( c in B & a \/ a' c= c implies b \/ b' c= c )
assume A17: ( c in B & a \/ a' c= c ) ; :: thesis: b \/ b' c= c
then ( a c= c & a' c= c ) by XBOOLE_1:11;
then ( b c= c & b' c= c ) by A3, A15, A16, A17;
hence b \/ b' c= c by XBOOLE_1:8; :: thesis: verum

end;

hence [(a \/ a'),(b \/ b')] in X deps_encl_by B ; :: thesis: verum

end;

end;

end;