[STATEMENT]
lemma Basis_S_transfer[transfer_rule]: "rel_set cr_S Basis Basis_S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_set cr_S Basis Basis_S
[PROOF STEP]
using Abs_inverse rep_inverse basis_subset
[PROOF STATE]
proof (prove)
using this:
?y \<in> S \<Longrightarrow> rep (Abs ?y) = ?y
Abs (rep ?x) = ?x
Basis \<subseteq> S

goal (1 subgoal):
 1. rel_set cr_S Basis Basis_S
[PROOF STEP]
by (force simp: rel_set_def Basis_S_def cr_S_def)