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