let p be polyhedron; :: thesis: for k being Integer
for c, d being Element of (k -chain-space p) holds
( c = d iff for x being Element of k -polytopes p holds
( x in c iff x in d ) )
let k be Integer; :: thesis: for c, d being Element of (k -chain-space p) holds
( c = d iff for x being Element of k -polytopes p holds
( x in c iff x in d ) )
let c, d be Element of (k -chain-space p); :: thesis: ( c = d iff for x being Element of k -polytopes p holds
( x in c iff x in d ) )
thus ( c = d implies for x being Element of k -polytopes p holds
( x in c iff x in d ) ) ; :: thesis: ( ( for x being Element of k -polytopes p holds
( x in c iff x in d ) ) implies c = d )
thus ( ( for x being Element of k -polytopes p holds
( x in c iff x in d ) ) implies c = d ) :: thesis: verum

proof

assume A1: for x being Element of k -polytopes p holds
( x in c iff x in d ) ; :: thesis: c = d
assume c <> d ; :: thesis: contradiction
then consider x being Element of k -polytopes p such that
A2: c @ x <> d @ x by Th41;
( ( x in c & not x in d ) or ( x in d & not x in c ) ) by A2, BSPACE:13;
hence contradiction by A1; :: thesis: verum

end;