let AS be AffinSpace; for a, b, x, y, z, t being Element of AS 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 AS; ( 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 that
A1:
a <> b
and
A2:
( ( 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 ) )
; x,y // z,t
A3:
a,b // z,t
by A2, Th3;
a,b // x,y
by A2, Th3;
hence
x,y // z,t
by A1, A3, DIRAF:40; verum