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 {(R#2 S)} /\ D = {(R#2 S)} & {(R#3b S)} /\ D = {(R#3b S)} & D /\ {(R#3e S)} = {(R#3e S)} & X is D -expanded & [x1,x2] in |.(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 {(R#2 S)} /\ D = {(R#2 S)} & {(R#3b S)} /\ D = {(R#3b S)} & D /\ {(R#3e S)} = {(R#3e S)} & X is D -expanded & [x1,x2] in |.(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 {(R#2 S)} /\ D = {(R#2 S)} & {(R#3b S)} /\ D = {(R#3b S)} & D /\ {(R#3e S)} = {(R#3e S)} & X is D -expanded & [x1,x2] in |.(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: ( {(R#2 S)} /\ D = {(R#2 S)} & {(R#3b S)} /\ D = {(R#3b S)} & D /\ {(R#3e S)} = {(R#3e S)} & X is D -expanded & [x1,x2] in |.(ar r).| -placesOf ((X,D) -termEq) implies ( (r -compound) . x1 in X iff (r -compound) . x2 in X ) )
set s = r;
set n = |.(ar r).|;
set AT = AllTermsOf S;
set E = TheEqSymbOf S;
set Phi = X;
set f = r -compound ;
set R = (X,D) -termEq ;
assume A1: ( {(R#2 S)} /\ D = {(R#2 S)} & {(R#3b S)} /\ D = {(R#3b S)} & D /\ {(R#3e S)} = {(R#3e S)} & X is D -expanded & [x1,x2] in |.(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 Lm31, Lm32;
thus ( (r -compound) . x1 in X implies (r -compound) . x2 in X ) by A1, Lm39; :: thesis: ( (r -compound) . x2 in X implies (r -compound) . x1 in X )
reconsider RR = |.(ar r).| -placesOf Rr as total symmetric Relation of (|.(ar r).| -tuples_on (AllTermsOf S)) ;
[x2,x1] in RR by EQREL_1:6, A1;
hence ( (r -compound) . x2 in X implies (r -compound) . x1 in X ) by A1, Lm39; :: thesis: verum