let AS be AffinSpace; :: thesis: 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; :: 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 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 ) ) ; :: thesis: 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; :: thesis: verum