let E be set ; for S being semi-Thue-system of E st S is Thue-system of E holds
==>.-relation S = (==>.-relation S) ~
let S be semi-Thue-system of E; ( S is Thue-system of E implies ==>.-relation S = (==>.-relation S) ~ )
assume A1:
S is Thue-system of E
; ==>.-relation S = (==>.-relation S) ~
now for x being object holds
( ( x in ==>.-relation S implies x in (==>.-relation S) ~ ) & ( x in (==>.-relation S) ~ implies x in ==>.-relation S ) )let x be
object ;
( ( x in ==>.-relation S implies x in (==>.-relation S) ~ ) & ( x in (==>.-relation S) ~ implies x in ==>.-relation S ) )thus
(
x in ==>.-relation S implies
x in (==>.-relation S) ~ )
( x in (==>.-relation S) ~ implies x in ==>.-relation S )proof
assume A2:
x in ==>.-relation S
;
x in (==>.-relation S) ~
then consider a,
b being
object such that A3:
(
a in E ^omega &
b in E ^omega )
and A4:
x = [a,b]
by ZFMISC_1:def 2;
reconsider a =
a,
b =
b as
Element of
E ^omega by A3;
a ==>. b,
S
by A2, A4, Def6;
then
b ==>. a,
S
by A1, Th17;
then
[b,a] in ==>.-relation S
by Def6;
hence
x in (==>.-relation S) ~
by A4, RELAT_1:def 7;
verum
end; thus
(
x in (==>.-relation S) ~ implies
x in ==>.-relation S )
verumproof
assume A5:
x in (==>.-relation S) ~
;
x in ==>.-relation S
then consider a,
b being
object such that A6:
(
a in E ^omega &
b in E ^omega )
and A7:
x = [a,b]
by ZFMISC_1:def 2;
reconsider a =
a,
b =
b as
Element of
E ^omega by A6;
[b,a] in ==>.-relation S
by A5, A7, RELAT_1:def 7;
then
b ==>. a,
S
by Def6;
then
a ==>. b,
S
by A1, Th17;
hence
x in ==>.-relation S
by A7, Def6;
verum
end; end;
hence
==>.-relation S = (==>.-relation S) ~
by TARSKI:2; verum