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 b1 being object st
( b1 in X & ( for b2 being object holds
( not b2 in X or b1 = b2 or not [b1,b2] in R ) ) ) )
assume ( X c= field R & X <> {} ) ; :: thesis: ex b1 being object st
( b1 in X & ( for b2 being object holds
( not b2 in X or b1 = b2 or not [b1,b2] in R ) ) )
hence ex b1 being object st
( b1 in X & ( for b2 being object holds
( not b2 in X or b1 = b2 or not [b1,b2] in R ) ) ) by A2; :: thesis: verum