let X be Element of Components R; :: thesis: not X is empty
consider x being set such that
A1: ( x in the carrier of R & X = Class (Path_Rel R),x ) by EQREL_1:def 5;
thus not X is empty by A1, EQREL_1:28; :: thesis: verum