let X be finite set ; :: thesis: for M, F being Dependency-set of X st M is (M1) & M is (M2) & M is (M3) & F = { [A,B] where A, B is Subset of X : ex A9, B9 being Subset of X st
( [A9,B9] >= [A,B] & [A9,B9] in M ) } holds
( M = Maximal_wrt F & F is full_family & ( for G being Full-family of X st M = Maximal_wrt G holds
G = F ) )
let M, F be Dependency-set of X; :: thesis: ( M is (M1) & M is (M2) & M is (M3) & F = { [A,B] where A, B is Subset of X : ex A9, B9 being Subset of X st
( [A9,B9] >= [A,B] & [A9,B9] in M ) } implies ( M = Maximal_wrt F & F is full_family & ( for G being Full-family of X st M = Maximal_wrt G holds
G = F ) ) )
assume that
A1: ( M is (M1) & M is (M2) & M is (M3) ) and
A2: F = { [A,B] where A, B is Subset of X : ex A9, B9 being Subset of X st
( [A9,B9] >= [A,B] & [A9,B9] in M ) } ; :: thesis: ( M = Maximal_wrt F & F is full_family & ( for G being Full-family of X st M = Maximal_wrt G holds
G = F ) )
A3: F is (F1)
proof
let A be Subset of X; :: according to ARMSTRNG:def 11 :: thesis: [A,A] in F
ex A9, B9 being Subset of X st
( [A9,B9] >= [A,A] & [A9,B9] in M ) by A1;
hence [A,A] in F by A2; :: thesis: verum
end;
A4: now :: thesis: for x being set st x in F holds
ex a, b, a9, b9 being Subset of X st
( x = [a,b] & [a9,b9] >= [a,b] & [a9,b9] in M )
let x be set ; :: thesis: ( x in F implies ex a, b, a9, b9 being Subset of X st
( x = [a,b] & [a9,b9] >= [a,b] & [a9,b9] in M ) )
assume x in F ; :: thesis: ex a, b, a9, b9 being Subset of X st
( x = [a,b] & [a9,b9] >= [a,b] & [a9,b9] in M )
then consider a, b being Subset of X such that
A5: x = [a,b] and
A6: ex a9, b9 being Subset of X st
( [a9,b9] >= [a,b] & [a9,b9] in M ) by A2;
consider a9, b9 being Subset of X such that
A7: [a9,b9] >= [a,b] and
A8: [a9,b9] in M by A6;
take a = a; :: thesis: ex b, a9, b9 being Subset of X st
( x = [a,b] & [a9,b9] >= [a,b] & [a9,b9] in M )
take b = b; :: thesis: ex a9, b9 being Subset of X st
( x = [a,b] & [a9,b9] >= [a,b] & [a9,b9] in M )
take a9 = a9; :: thesis: ex b9 being Subset of X st
( x = [a,b] & [a9,b9] >= [a,b] & [a9,b9] in M )
take b9 = b9; :: thesis: ( x = [a,b] & [a9,b9] >= [a,b] & [a9,b9] in M )
thus ( x = [a,b] & [a9,b9] >= [a,b] & [a9,b9] in M ) by A5, A7, A8; :: thesis: verum
end;
A9: now :: thesis: for A, B being Subset of X st [A,B] in F holds
ex a9, b9 being Subset of X st
( [a9,b9] >= [A,B] & [a9,b9] in M )
let A, B be Subset of X; :: thesis: ( [A,B] in F implies ex a9, b9 being Subset of X st
( [a9,b9] >= [A,B] & [a9,b9] in M ) )
assume [A,B] in F ; :: thesis: ex a9, b9 being Subset of X st
( [a9,b9] >= [A,B] & [a9,b9] in M )
then consider a, b, a9, b9 being Subset of X such that
A10: [A,B] = [a,b] and
A11: [a9,b9] >= [a,b] and
A12: [a9,b9] in M by A4;
take a9 = a9; :: thesis: ex b9 being Subset of X st
( [a9,b9] >= [A,B] & [a9,b9] in M )
take b9 = b9; :: thesis: ( [a9,b9] >= [A,B] & [a9,b9] in M )
thus ( [a9,b9] >= [A,B] & [a9,b9] in M ) by A10, A11, A12; :: 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
A13: [A,B] in F and
A14: [B,C] in F ; :: thesis: [A,C] in F
consider A9, B9 being Subset of X such that
A15: [A9,B9] >= [A,B] and
A16: [A9,B9] in M by A9, A13;
consider B19, C9 being Subset of X such that
A17: [B19,C9] >= [B,C] and
A18: [B19,C9] in M by A9, A14;
A19: B19 c= B by A17;
B c= B9 by A15;
then B19 c= B9 by A19;
then C9 c= B9 by A1, A16, A18;
then A20: [A9,B9] >= [A9,C9] ;
A21: C c= C9 by A17;
A9 c= A by A15;
then [A9,C9] >= [A,C] by A21;
then [A9,B9] >= [A,C] by A20, Th12;
hence [A,C] in F by A2, A16; :: thesis: verum
end;
then A22: F is (F2) by Th18;
A23: 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
A24: [A,B] in F and
A25: [A9,B9] in F ; :: thesis: [(A \/ A9),(B \/ B9)] in F
consider a1, b1 being Subset of X such that
A26: [a1,b1] >= [A,B] and
A27: [a1,b1] in M by A9, A24;
A28: B c= b1 by A26;
consider a19, b19 being Subset of X such that
A29: [a19,b19] >= [A9,B9] and
A30: [a19,b19] in M by A9, A25;
A31: B9 c= b19 by A29;
consider A99, B99 being Subset of X such that
A32: [A99,B99] >= [(A \/ A9),(A \/ A9)] and
A33: [A99,B99] in M by A1;
A34: A \/ A9 c= B99 by A32;
a19 c= A9 by A29;
then a19 c= A \/ A9 by XBOOLE_1:10;
then a19 c= B99 by A34;
then b19 c= B99 by A1, A33, A30;
then A35: B9 c= B99 by A31;
a1 c= A by A26;
then a1 c= A \/ A9 by XBOOLE_1:10;
then a1 c= B99 by A34;
then b1 c= B99 by A1, A33, A27;
then B c= B99 by A28;
then A36: B \/ B9 c= B99 \/ B99 by A35, XBOOLE_1:13;
A99 c= A \/ A9 by A32;
then [A99,B99] >= [(A \/ A9),(B \/ B9)] by A36;
hence [(A \/ A9),(B \/ B9)] in F by A2, A33; :: thesis: verum
end;
set DOX = Dependencies-Order X;
now :: thesis: for x being object holds
( ( x in M implies x in Maximal_wrt F ) & ( x in Maximal_wrt F implies x in M ) )
let x be object ; :: thesis: ( ( x in M implies x in Maximal_wrt F ) & ( x in Maximal_wrt F implies x in M ) )
hereby :: thesis: ( x in Maximal_wrt F implies x in M )
assume A37: x in M ; :: thesis: x in Maximal_wrt F
then consider a, b being Subset of X such that
A38: x = [a,b] by Th9;
x is_maximal_wrt F, Dependencies-Order X
proof
thus x in F by A2, A37, A38; :: according to WAYBEL_4:def 23 :: thesis: for b1 being set holds
( not b1 in F or b1 = x or not [x,b1] in Dependencies-Order X )
given y being set such that A39: y in F and
A40: y <> x and
A41: [x,y] in Dependencies-Order X ; :: thesis: contradiction
consider e, f being Dependency of X such that
A42: [x,y] = [e,f] and
A43: e <= f by A41;
A44: y = f by A42, XTUPLE_0:1;
consider c, d, c9, d9 being Subset of X such that
A45: y = [c,d] and
A46: [c9,d9] >= [c,d] and
A47: [c9,d9] in M by A4, A39;
A48: x = e by A42, XTUPLE_0:1;
then A49: [c9,d9] >= [a,b] by A38, A43, A44, A45, A46, Th12;
then A50: d9 = b by A1, A37, A38, A47;
c9 = a by A1, A37, A38, A47, A49;
hence contradiction by A38, A40, A43, A48, A44, A45, A46, A50, Th11; :: thesis: verum
end;
hence x in Maximal_wrt F by Def1; :: thesis: verum
end;
assume A51: x in Maximal_wrt F ; :: thesis: x in M
then A52: x is_maximal_wrt F, Dependencies-Order X by Def1;
assume A53: not x in M ; :: thesis: contradiction
consider a, b, a9, b9 being Subset of X such that
A54: x = [a,b] and
A55: [a9,b9] >= [a,b] and
A56: [a9,b9] in M by A4, A51;
A57: [[a,b],[a9,b9]] in Dependencies-Order X by A55;
[a9,b9] in F by A2, A56;
hence contradiction by A52, A54, A56, A53, A57; :: thesis: verum
end;
hence M = Maximal_wrt F by TARSKI:2; :: thesis: ( F is full_family & ( for G being Full-family of X st M = Maximal_wrt G holds
G = F ) )
F is (F3)
proof
let A, B, A9, B9 be Subset of X; :: according to ARMSTRNG:def 12 :: thesis: ( [A,B] in F & [A,B] >= [A9,B9] implies [A9,B9] in F )
assume that
A58: [A,B] in F and
A59: [A,B] >= [A9,B9] ; :: thesis: [A9,B9] in F
consider a9, b9 being Subset of X such that
A60: [a9,b9] >= [A,B] and
A61: [a9,b9] in M by A9, A58;
[a9,b9] >= [A9,B9] by A59, A60, Th12;
hence [A9,B9] in F by A2, A61; :: thesis: verum
end;
hence F is full_family by A3, A22, A23; :: thesis: for G being Full-family of X st M = Maximal_wrt G holds
G = F
let G be Full-family of X; :: thesis: ( M = Maximal_wrt G implies G = F )
assume A62: M = Maximal_wrt G ; :: thesis: G = F
now :: thesis: for x being object holds
( ( x in G implies x in F ) & ( x in F implies x in G ) )
let x be object ; :: thesis: ( ( x in G implies x in F ) & ( x in F implies x in G ) )
hereby :: thesis: ( x in F implies x in G )
A63: field (Dependencies-Order X) = [:(bool X),(bool X):] by Th17;
assume A64: x in G ; :: thesis: x in F
then consider a, b being Subset of X such that
A65: x = [a,b] by Th9;
defpred S1[ object ] means ex y being Dependency of X st
( $1 = y & y >= [a,b] );
consider MA being set such that
A66: for x being object holds
( x in MA iff ( x in G & S1[x] ) ) from XBOOLE_0:sch 1();
 MA c= G by A66;
then A67: MA is finite Subset of (field (Dependencies-Order X)) by A63, XBOOLE_1:1;
MA <> {} by A64, A65, A66;
then consider m being Element of MA such that
A68: m is_maximal_wrt MA, Dependencies-Order X by A67, Th2;
A69: m in MA by A68;
then m in G by A66;
then A70: ex a9, b9 being Subset of X st m = [a9,b9] by Th9;
m is_maximal_wrt G, Dependencies-Order X
proof
A71: ex mm being Dependency of X st
( m = mm & mm >= [a,b] ) by A66, A69;
thus m in G by A66, A69; :: according to WAYBEL_4:def 23 :: thesis: for b1 being set holds
( not b1 in G or b1 = m or not [m,b1] in Dependencies-Order X )
given y being set such that A72: y in G and
A73: y <> m and
A74: [m,y] in Dependencies-Order X ; :: thesis: contradiction
consider e, f being Dependency of X such that
A75: [m,y] = [e,f] and
A76: e <= f by A74;
A77: y = f by A75, XTUPLE_0:1;
m = e by A75, XTUPLE_0:1;
then f >= [a,b] by A71, A76, Th12;
then y in MA by A66, A72, A77;
hence contradiction by A68, A73, A74; :: thesis: verum
end;
then A78: m in (Dependencies-Order X) Maximal_in G by Def1;
ex y being Dependency of X st
( m = y & y >= [a,b] ) by A66, A69;
hence x in F by A2, A62, A65, A78, A70; :: thesis: verum
end;
assume x in F ; :: thesis: x in G
then ex a, b, a1, b1 being Subset of X st
( x = [a,b] & [a1,b1] >= [a,b] & [a1,b1] in M ) by A4;
hence x in G by A62, Def12; :: thesis: verum
end;
hence G = F by TARSKI:2; :: thesis: verum