consider a, b being Element of AS such that
A1: a <> b by DIRAF:40;
set A = Line (a,b);
Line (a,b) is being_line by A1, AFF_1:def 3;
then Line (a,b) in AfLines AS ;
then Class ((LinesParallelity AS),(Line (a,b))) in Class (LinesParallelity AS) by EQREL_1:def 3;
hence Class (LinesParallelity AS) is non empty set ; :: thesis: verum