let S be Language; :: thesis: for s being low-compounding Element of S
for T, U being abs (ar b₁) -element Element of (AllTermsOf S) * st s is termal holds
{[(PairWiseEq (T,U)),((<*(TheEqSymbOf S)*> ^ (s -compound T)) ^ (s -compound U))]} is {} ,{(R3d S)} -derivable
let s be low-compounding Element of S; :: thesis: for T, U being abs (ar s) -element Element of (AllTermsOf S) * st s is termal holds
{[(PairWiseEq (T,U)),((<*(TheEqSymbOf S)*> ^ (s -compound T)) ^ (s -compound U))]} is {} ,{(R3d S)} -derivable
set m = abs (ar s);
set AT = AllTermsOf S;
set E = TheEqSymbOf S;
let T, U be abs (ar s) -element Element of (AllTermsOf S) * ; :: thesis: ( s is termal implies {[(PairWiseEq (T,U)),((<*(TheEqSymbOf S)*> ^ (s -compound T)) ^ (s -compound U))]} is {} ,{(R3d S)} -derivable )
assume s is termal ; :: thesis: {[(PairWiseEq (T,U)),((<*(TheEqSymbOf S)*> ^ (s -compound T)) ^ (s -compound U))]} is {} ,{(R3d S)} -derivable
then reconsider ss = s as termal Element of S ;
reconsider t1 = ss -compound T, t2 = ss -compound U as termal string of S ;
reconsider conclusion = (<*(TheEqSymbOf S)*> ^ t1) ^ t2 as wff string of S ;
reconsider seqt = [(PairWiseEq (T,U)),conclusion] as Element of S -sequents by DefSeqtLike;
reconsider Seqts = {} as Subset of (S -sequents) by XBOOLE_1:2;
ss is termal ;
then B0: ( s is operational & seqt `1 = PairWiseEq (T,U) & seqt `2 = (<*(TheEqSymbOf S)*> ^ (s -compound T)) ^ (s -compound U) ) by MCART_1:7;
seqt Rule3d Seqts by B0, Def3d;
then [Seqts,seqt] in P3d S by DefP3d;
then seqt in (R3d S) . Seqts by Lm1;
then {seqt} c= (R3d S) . Seqts by ZFMISC_1:31;
hence {[(PairWiseEq (T,U)),((<*(TheEqSymbOf S)*> ^ (s -compound T)) ^ (s -compound U))]} is {} ,{(R3d S)} -derivable by Lm9; :: thesis: verum