let OAS be OAffinSpace; :: thesis: OAS is CongrSpace-like
thus for x, y, z, t, a, b being Element of OAS st x,y // a,b & a,b // z,t & a <> b holds
x,y // z,t by DIRAF:6; :: according to TRANSGEO:def 5 :: thesis: ( ( for x, y, z being Element of OAS holds x,x // y,z ) & ( for x, y, z, t being Element of OAS st x,y // z,t holds
z,t // x,y ) & ( for x, y being Element of OAS holds x,y // x,y ) )
thus for x, y, z being Element of OAS holds x,x // y,z by DIRAF:7; :: thesis: ( ( for x, y, z, t being Element of OAS st x,y // z,t holds
z,t // x,y ) & ( for x, y being Element of OAS holds x,y // x,y ) )
thus for x, y, z, t being Element of OAS st x,y // z,t holds
z,t // x,y by DIRAF:5; :: thesis: for x, y being Element of OAS holds x,y // x,y
thus for x, y being Element of OAS holds x,y // x,y by DIRAF:4; :: thesis: verum