let E be set ; :: thesis: 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; :: thesis: ( S is Thue-system of E implies ==>.-relation S = (==>.-relation S) ~ )

assume A1: S is Thue-system of E ; :: thesis: ==>.-relation S = (==>.-relation S) ~

==>.-relation S = (==>.-relation S) ~

let S be semi-Thue-system of E; :: thesis: ( S is Thue-system of E implies ==>.-relation S = (==>.-relation S) ~ )

assume A1: S is Thue-system of E ; :: thesis: ==>.-relation S = (==>.-relation S) ~

now :: thesis: for x being object holds

( ( x in ==>.-relation S implies x in (==>.-relation S) ~ ) & ( x in (==>.-relation S) ~ implies x in ==>.-relation S ) )

hence
==>.-relation S = (==>.-relation S) ~
by TARSKI:2; :: thesis: verum( ( x in ==>.-relation S implies x in (==>.-relation S) ~ ) & ( x in (==>.-relation S) ~ implies x in ==>.-relation S ) )

let x be object ; :: thesis: ( ( 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) ~ ) :: thesis: ( x in (==>.-relation S) ~ implies x in ==>.-relation S )

end;thus ( x in ==>.-relation S implies x in (==>.-relation S) ~ ) :: thesis: ( x in (==>.-relation S) ~ implies x in ==>.-relation S )

proof

thus
( x in (==>.-relation S) ~ implies x in ==>.-relation S )
:: thesis: verum
assume A2:
x in ==>.-relation S
; :: thesis: 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; :: thesis: verum

end;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; :: thesis: verum

proof

assume A5:
x in (==>.-relation S) ~
; :: thesis: 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; :: thesis: verum

end;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; :: thesis: verum