consider a, b being Element of AS such that
A1: a <> b by DIRAF:47;
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 5;
hence Class (LinesParallelity AS) is non empty set ; :: thesis: verum