reconsider R = {[0 ,1]} as non empty Relation ;
take R ; :: thesis: R is complete
A1: field R = {0 ,1} by RELAT_1:32;
thus R is confluent :: according to REWRITE1:def 25 :: thesis: R is strongly-normalizing

proof

let a, b be set ; :: according to REWRITE1:def 22 :: thesis: ( a,b are_divergent_wrt R implies a,b are_convergent_wrt R )
given c being set such that A2: ( R reduces c,a & R reduces c,b ) ; :: according to REWRITE1:def 8 :: thesis: a,b are_convergent_wrt R

per cases ( a = b or a <> b ) ;

suppose a = b ; :: thesis: a,b are_convergent_wrt R

hence a,b are_convergent_wrt R by Th39; :: thesis: verum

end;

suppose a <> b ; :: thesis: a,b are_convergent_wrt R

then ( a <> c or b <> c ) ;
then c in field R by A2, Th19;
then ( a in {0 ,1} & b in {0 ,1} & [0 ,1] in R ) by A1, A2, Th19, TARSKI:def 1;
then ( ( a = 0 or a = 1 ) & ( b = 0 or b = 1 ) & R reduces 0 ,1 & R reduces 1,1 ) by Th13, Th16, TARSKI:def 2;
hence a,b are_convergent_wrt R by Def7; :: thesis: verum

end;

end;

end;

A3: R is irreflexive

proof

let x be set ; :: according to RELAT_2:def 2,RELAT_2:def 10 :: thesis: ( not x in field R or not [x,x] in R )
assume ( x in field R & [x,x] in R ) ; :: thesis: contradiction
then [x,x] = [0 ,1] by TARSKI:def 1;
then ( x = 0 & x = 1 ) by ZFMISC_1:33;
hence contradiction ; :: thesis: verum

end;

R is co-well_founded

proof

let Y be set ; :: according to REWRITE1:def 16 :: thesis: ( Y c= field R & Y <> {} implies ex a being set st
( a in Y & ( for b being set st b in Y & a <> b holds
not [a,b] in R ) ) )
assume A4: ( Y c= field R & Y <> {} ) ; :: thesis: ex a being set st
( a in Y & ( for b being set st b in Y & a <> b holds
not [a,b] in R ) )
then reconsider Y' = Y as non empty set ;
consider y being Element of Y';

per cases ( 1 in Y or ( not 1 in Y & y in Y ) ) ;

suppose A5: 1 in Y ; :: thesis: ex a being set st
( a in Y & ( for b being set st b in Y & a <> b holds
not [a,b] in R ) )

take 1 ; :: thesis: ( 1 in Y & ( for b being set st b in Y & 1 <> b holds
not [1,b] in R ) )
thus 1 in Y by A5; :: thesis: for b being set st b in Y & 1 <> b holds
not [1,b] in R
let b be set ; :: thesis: ( b in Y & 1 <> b implies not [1,b] in R )
assume ( b in Y & 1 <> b ) ; :: thesis: not [1,b] in R
[0 ,1] <> [1,b] by ZFMISC_1:33;
hence not [1,b] in R by TARSKI:def 1; :: thesis: verum

end;

suppose A6: ( not 1 in Y & y in Y ) ; :: thesis: ex a being set st
( a in Y & ( for b being set st b in Y & a <> b holds
not [a,b] in R ) )

take 0 ; :: thesis: ( 0 in Y & ( for b being set st b in Y & 0 <> b holds
not [0 ,b] in R ) )
thus 0 in Y by A1, A4, A6, TARSKI:def 2; :: thesis: for b being set st b in Y & 0 <> b holds
not [0 ,b] in R
let b be set ; :: thesis: ( b in Y & 0 <> b implies not [0 ,b] in R )
assume b in Y ; :: thesis: ( not 0 <> b or not [0 ,b] in R )
hence ( not 0 <> b or not [0 ,b] in R ) by A1, A4, A6, TARSKI:def 2; :: thesis: verum

end;

end;

end;

then R is irreflexive co-well_founded Relation by A3;
hence R is strongly-normalizing ; :: thesis: verum