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 c @ x = d @ x )
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 c @ x = d @ x )
let c, d be Element of (k -chain-space p); :: thesis: ( c = d iff for x being Element of k -polytopes p holds c @ x = d @ x )
thus ( c = d implies for x being Element of k -polytopes p holds c @ x = d @ x ) ; :: thesis: ( ( for x being Element of k -polytopes p holds c @ x = d @ x ) implies c = d )
thus ( ( for x being Element of k -polytopes p holds c @ x = d @ x ) implies c = d ) :: thesis: verum

proof

assume A1: for x being Element of k -polytopes p holds c @ x = d @ x ; :: thesis: c = d
thus c c= d :: according to XBOOLE_0:def 10 :: thesis: d c= c

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in c or x in d )
assume A2: x in c ; :: thesis: x in d
reconsider x = x as Element of k -polytopes p by A2;
reconsider c = c as Subset of (k -polytopes p) ;
c @ x = 1. Z_2 by A2, BSPACE:def 3;
then d @ x = 1. Z_2 by A1;
hence x in d by BSPACE:9; :: thesis: verum

end;

thus d c= c :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in d or x in c )
assume A3: x in d ; :: thesis: x in c
reconsider x = x as Element of k -polytopes p by A3;
reconsider d = d as Subset of (k -polytopes p) ;
d @ x = 1. Z_2 by A3, BSPACE:def 3;
then c @ x = 1. Z_2 by A1;
hence x in c by BSPACE:9; :: thesis: verum

end;

end;