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 ( B is empty or not B is empty ) ;
suppose A1: B is empty ; :: thesis: X deps_encl_by B is full_family
now :: thesis: for x being object holds
( ( x in X deps_encl_by B implies x in Dependencies X ) & ( x in Dependencies X implies x in X deps_encl_by B ) )
let x be object ; :: 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 object such that
A2: x1 in bool X and
A3: x2 in bool X and
A4: x = [x1,x2] by ZFMISC_1:def 2;
reconsider x1 = x1, x2 = x2 as set by TARSKI:1;
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, A3, A4; :: 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 Th19;
hence X deps_encl_by B is full_family ; :: thesis: verum
end;
suppose not B is empty ; :: thesis: X deps_encl_by B is full_family
then reconsider B = B as non empty Subset-Family of X ;
thus X deps_encl_by B is (F1) :: according to ARMSTRNG:def 14 :: 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 11 :: 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;
A5: now :: thesis: for x, y being Subset of X
for c being Element of B st [x,y] in X deps_encl_by B & x c= c holds
y c= c
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
A6: [x,y] in X deps_encl_by B and
A7: x c= c ; :: thesis: y c= c
consider a, b being Subset of X such that
A8: [x,y] = [a,b] and
A9: for c being set st c in B & a c= c holds
b c= c by A6;
A10: y = b by A8, XTUPLE_0:1;
x = a by A8, XTUPLE_0:1;
hence y c= c by A7, A9, A10; :: thesis: verum
end;
now :: thesis: for a, b, c being Subset of X st [a,b] in X deps_encl_by B & [b,c] in X deps_encl_by B holds
[a,c] in X deps_encl_by B
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
A11: [a,b] in X deps_encl_by B and
A12: [b,c] in X deps_encl_by B ; :: thesis: [a,c] in X deps_encl_by B
now :: thesis: for x being set st x in B & a c= x holds
c c= x
let x be set ; :: thesis: ( x in B & a c= x implies c c= x )
assume that
A13: x in B and
A14: a c= x ; :: thesis: c c= x
b c= x by A5, A11, A13, A14;
hence c c= x by A5, A12, A13; :: thesis: verum
end;
hence [a,c] in X deps_encl_by B ; :: thesis: verum
end;
hence X deps_encl_by B is (F2) by Th18; :: 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, a9, b9 be Subset of X; :: according to ARMSTRNG:def 12 :: thesis: ( [a,b] in X deps_encl_by B & [a,b] >= [a9,b9] implies [a9,b9] in X deps_encl_by B )
assume that
A15: [a,b] in X deps_encl_by B and
A16: [a,b] >= [a9,b9] ; :: thesis: [a9,b9] in X deps_encl_by B
A17: b9 c= b by A16;
A18: a c= a9 by A16;
now :: thesis: for c being set st c in B & a9 c= c holds
b9 c= c
let c be set ; :: thesis: ( c in B & a9 c= c implies b9 c= c )
assume that
A19: c in B and
A20: a9 c= c ; :: thesis: b9 c= c
a c= c by A18, A20;
then b c= c by A5, A15, A19;
hence b9 c= c by A17; :: thesis: verum
end;
hence [a9,b9] in X deps_encl_by B ; :: thesis: verum
end;
thus X deps_encl_by B is (F4) :: thesis: verum
proof
let a, b, a9, b9 be Subset of X; :: according to ARMSTRNG:def 13 :: thesis: ( [a,b] in X deps_encl_by B & [a9,b9] in X deps_encl_by B implies [(a \/ a9),(b \/ b9)] in X deps_encl_by B )
assume that
A21: [a,b] in X deps_encl_by B and
A22: [a9,b9] in X deps_encl_by B ; :: thesis: [(a \/ a9),(b \/ b9)] in X deps_encl_by B
now :: thesis: for c being set st c in B & a \/ a9 c= c holds
b \/ b9 c= c
let c be set ; :: thesis: ( c in B & a \/ a9 c= c implies b \/ b9 c= c )
assume that
A23: c in B and
A24: a \/ a9 c= c ; :: thesis: b \/ b9 c= c
a9 c= c by A24, XBOOLE_1:11;
then A25: b9 c= c by A5, A22, A23;
a c= c by A24, XBOOLE_1:11;
then b c= c by A5, A21, A23;
hence b \/ b9 c= c by A25, XBOOLE_1:8; :: thesis: verum
end;
hence [(a \/ a9),(b \/ b9)] in X deps_encl_by B ; :: thesis: verum
end;
end;
end;