thus ( x,y are_collinear implies ex l being Block of S st {x,y} c= l ) :: thesis: ( ex l being Block of S st {x,y} c= l implies x,y are_collinear )

proof

assume A1: x,y are_collinear ; :: thesis: ex l being Block of S st {x,y} c= l

per cases ( x = y or x <> y ) ;

suppose A2: x = y ; :: thesis: ex l being Block of S st {x,y} c= l

consider l being Block of S such that
A3: x in l by Def9;
take l ; :: thesis: {x,y} c= l
thus {x,y} c= l by A2, A3, ZFMISC_1:32; :: thesis: verum

end;

suppose x <> y ; :: thesis: ex l being Block of S st {x,y} c= l

hence ex l being Block of S st {x,y} c= l by A1; :: thesis: verum

end;

end;

end;

given l being Block of S such that A4: {x,y} c= l ; :: thesis: x,y are_collinear
thus x,y are_collinear by A4; :: thesis: verum