let R be RelStr ; :: thesis: ( R is empty implies R is void )
assume R is empty ; :: thesis: R is void
then reconsider R1 = R as empty RelStr ;
the InternalRel of R1 is empty ;
hence the InternalRel of R is empty ; :: according to YELLOW_3:def 3 :: thesis: verum