let X, x1, x2 be set ; :: thesis: for S being Language
for r being relational Element of S
for D being RuleSet of S st {(R2 S)} /\ D = {(R2 S)} & {(R3b S)} /\ D = {(R3b S)} & D /\ {(R3e S)} = {(R3e S)} & X is D -expanded & [x1,x2] in (abs (ar r)) -placesOf ((X,D) -termEq) holds
( (r -compound) . x1 in X iff (r -compound) . x2 in X )
let S be Language; :: thesis: for r being relational Element of S
for D being RuleSet of S st {(R2 S)} /\ D = {(R2 S)} & {(R3b S)} /\ D = {(R3b S)} & D /\ {(R3e S)} = {(R3e S)} & X is D -expanded & [x1,x2] in (abs (ar r)) -placesOf ((X,D) -termEq) holds
( (r -compound) . x1 in X iff (r -compound) . x2 in X )
let r be relational Element of S; :: thesis: for D being RuleSet of S st {(R2 S)} /\ D = {(R2 S)} & {(R3b S)} /\ D = {(R3b S)} & D /\ {(R3e S)} = {(R3e S)} & X is D -expanded & [x1,x2] in (abs (ar r)) -placesOf ((X,D) -termEq) holds
( (r -compound) . x1 in X iff (r -compound) . x2 in X )
let D be RuleSet of S; :: thesis: ( {(R2 S)} /\ D = {(R2 S)} & {(R3b S)} /\ D = {(R3b S)} & D /\ {(R3e S)} = {(R3e S)} & X is D -expanded & [x1,x2] in (abs (ar r)) -placesOf ((X,D) -termEq) implies ( (r -compound) . x1 in X iff (r -compound) . x2 in X ) )
set s = r;
set n = abs (ar r);
set AT = AllTermsOf S;
set E = TheEqSymbOf S;
set Phi = X;
set f = r -compound ;
set R = (X,D) -termEq ;
assume B0: ( {(R2 S)} /\ D = {(R2 S)} & {(R3b S)} /\ D = {(R3b S)} & D /\ {(R3e S)} = {(R3e S)} & X is D -expanded & [x1,x2] in (abs (ar r)) -placesOf ((X,D) -termEq) ) ; :: thesis: ( (r -compound) . x1 in X iff (r -compound) . x2 in X )
then reconsider Rr = (X,D) -termEq as total symmetric Relation of (AllTermsOf S) by Lm24, Lm25;
thus ( (r -compound) . x1 in X implies (r -compound) . x2 in X ) by B0, Lm45; :: thesis: ( (r -compound) . x2 in X implies (r -compound) . x1 in X )
reconsider RR = (abs (ar r)) -placesOf Rr as total symmetric Relation of ((abs (ar r)) -tuples_on (AllTermsOf S)) ;
[x2,x1] in RR by B0, EQREL_1:6;
hence ( (r -compound) . x2 in X implies (r -compound) . x1 in X ) by B0, Lm45; :: thesis: verum