let AFS be AffinSpace; :: thesis: AFS is CongrSpace-like
thus for x, y, z, t, a, b being Element of AFS st x,y // a,b & a,b // z,t & a <> b holds
x,y // z,t by AFF_1:5; :: according to TRANSGEO:def 5 :: thesis: ( ( for x, y, z being Element of AFS holds x,x // y,z ) & ( for x, y, z, t being Element of AFS st x,y // z,t holds
z,t // x,y ) & ( for x, y being Element of AFS holds x,y // x,y ) )
thus for x, y, z being Element of AFS holds x,x // y,z by AFF_1:3; :: thesis: ( ( for x, y, z, t being Element of AFS st x,y // z,t holds
z,t // x,y ) & ( for x, y being Element of AFS holds x,y // x,y ) )
thus for x, y, z, t being Element of AFS st x,y // z,t holds
z,t // x,y by AFF_1:4; :: thesis: for x, y being Element of AFS holds x,y // x,y
thus for x, y being Element of AFS holds x,y // x,y by AFF_1:2; :: thesis: verum