per cases ( i in I or i nin dom R ) ;
suppose i in I ; :: thesis: for b1 being Relation st b1 = R . i holds
b1 is with_UN_property
hence for b1 being Relation st b1 = R . i holds
b1 is with_UN_property by Def17; :: thesis: verum
end;
suppose i nin dom R ; :: thesis: for b1 being Relation st b1 = R . i holds
b1 is with_UN_property
hence for b1 being Relation st b1 = R . i holds
b1 is with_UN_property by FUNCT_1:def 2; :: thesis: verum
end;
end;