let R be Relation; :: thesis: ( R is empty implies ( R is irreflexive & R is co-well_founded ) )
assume A1: R is empty ; :: thesis: ( R is irreflexive & R is co-well_founded )
then A2: ( dom R = {} & rng R = {} ) ;
thus R is irreflexive :: thesis: R is co-well_founded

proof

let x be object ; :: according to RELAT_2:def 2,RELAT_2:def 10 :: thesis: ( not x in field R or not [x,x] in R )
thus ( not x in field R or not [x,x] in R ) by A1; :: thesis: verum

end;

let X be set ; :: according to REWRITE1:def 16 :: thesis: ( not X c= field R or X = {} or ex b₁ being object st
( b₁ in X & ( for b₂ being object holds
( not b₂ in X or b₁ = b₂ or not [b₁,b₂] in R ) ) ) )
assume ( X c= field R & X <> {} ) ; :: thesis: ex b₁ being object st
( b₁ in X & ( for b₂ being object holds
( not b₂ in X or b₁ = b₂ or not [b₁,b₂] in R ) ) )
hence ex b₁ being object st
( b₁ in X & ( for b₂ being object holds
( not b₂ in X or b₁ = b₂ or not [b₁,b₂] in R ) ) ) by A2; :: thesis: verum