let A be non empty finite set ; :: thesis: for F, G being Dependency-set of A st charact_set F = charact_set G holds
Dependency-closure F = Dependency-closure G
let F, G be Dependency-set of A; :: thesis: ( charact_set F = charact_set G implies Dependency-closure F = Dependency-closure G )
assume A1: charact_set F = charact_set G ; :: thesis: Dependency-closure F = Dependency-closure G
set DCF = Dependency-closure F;
set DCG = Dependency-closure G;
now :: thesis: for x being object holds
( ( x in Dependency-closure F implies x in Dependency-closure G ) & ( x in Dependency-closure G implies x in Dependency-closure F ) )
let x be object ; :: thesis: ( ( x in Dependency-closure F implies x in Dependency-closure G ) & ( x in Dependency-closure G implies x in Dependency-closure F ) )
hereby :: thesis: ( x in Dependency-closure G implies x in Dependency-closure F )
assume A2: x in Dependency-closure F ; :: thesis: x in Dependency-closure G
then consider a, b being Subset of A such that
A3: x = [a,b] by Th9;
for c being Subset of A st a c= c & not b c= c holds
c in charact_set G by A1, A2, A3, Th57;
hence x in Dependency-closure G by A3, Th57; :: thesis: verum
end;
assume A4: x in Dependency-closure G ; :: thesis: x in Dependency-closure F
then consider a, b being Subset of A such that
A5: x = [a,b] by Th9;
for c being Subset of A st a c= c & not b c= c holds
c in charact_set F by A1, A4, A5, Th57;
hence x in Dependency-closure F by A5, Th57; :: thesis: verum
end;
hence Dependency-closure F = Dependency-closure G by TARSKI:2; :: thesis: verum