( 0. R in I & 0. R in J ) by Th2;
then 0. R in { x where x is Element of R : ( x in I & x in J ) } ;
hence not I /\ J is empty ; :: thesis: verum