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