let R be Relation; :: thesis: ( R is empty implies R is homogeneous )
assume A1: R is empty ; :: thesis: R is homogeneous
thus dom R is with_common_domain :: according to UNIALG_1:def 1 :: thesis: verum

proof

let x, y be Function; :: according to CARD_3:def 10 :: thesis: ( not x in dom R or not y in dom R or proj1 x = proj1 y )
assume x in dom R ; :: thesis: ( not y in dom R or proj1 x = proj1 y )
thus ( not y in dom R or proj1 x = proj1 y ) by A1; :: thesis: verum

end;