let R be non empty serial RelStr ; :: thesis: for x being Element of R holds Class ( the InternalRel of R,x) <> {}
let x be Element of R; :: thesis: Class ( the InternalRel of R,x) <> {}
A1: x in {x} by TARSKI:def 1;
consider y being object such that
A2: ( y in the carrier of R & [x,y] in the InternalRel of R ) by Def1, Def3;
thus Class ( the InternalRel of R,x) <> {} by RELAT_1:def 13, A2, A1; :: thesis: verum