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