per cases ( i in I or i nin dom R ) ;

suppose i in I ; :: thesis: for b₁ being Relation st b₁ = R . i holds
b₁ is with_UN_property

hence for b₁ being Relation st b₁ = R . i holds
b₁ is with_UN_property by Def17; :: thesis: verum

end;

suppose i nin dom R ; :: thesis: for b₁ being Relation st b₁ = R . i holds
b₁ is with_UN_property

hence for b₁ being Relation st b₁ = R . i holds
b₁ is with_UN_property by FUNCT_1:def 2; :: thesis: verum

end;

end;