let S be OAffinSpace; :: thesis: for a, b, x, y, z, t being Element of S st a <> b & ( ( a,b '||' x,y & a,b '||' z,t ) or ( a,b '||' x,y & z,t '||' a,b ) or ( x,y '||' a,b & z,t '||' a,b ) or ( x,y '||' a,b & a,b '||' z,t ) ) holds
x,y '||' z,t
let a, b, x, y, z, t be Element of S; :: thesis: ( a <> b & ( ( a,b '||' x,y & a,b '||' z,t ) or ( a,b '||' x,y & z,t '||' a,b ) or ( x,y '||' a,b & z,t '||' a,b ) or ( x,y '||' a,b & a,b '||' z,t ) ) implies x,y '||' z,t )
assume ( a <> b & ( ( a,b '||' x,y & a,b '||' z,t ) or ( a,b '||' x,y & z,t '||' a,b ) or ( x,y '||' a,b & z,t '||' a,b ) or ( x,y '||' a,b & a,b '||' z,t ) ) ) ; :: thesis: x,y '||' z,t
then ( a <> b & a,b '||' x,y & a,b '||' z,t ) by Th27;
hence x,y '||' z,t by Lm2; :: thesis: verum