let V be RealLinearSpace; :: thesis: for OAS being OAffinSpace st OAS = OASpace V holds
for a, b, c, d being Element of OAS
for u, v, w, y being VECTOR of V st a = u & b = v & c = w & d = y holds
( a,b '||' c,d iff u,v '||' w,y )
let OAS be OAffinSpace; :: thesis: ( OAS = OASpace V implies for a, b, c, d being Element of OAS
for u, v, w, y being VECTOR of V st a = u & b = v & c = w & d = y holds
( a,b '||' c,d iff u,v '||' w,y ) )
assume A1: OAS = OASpace V ; :: thesis: for a, b, c, d being Element of OAS
for u, v, w, y being VECTOR of V st a = u & b = v & c = w & d = y holds
( a,b '||' c,d iff u,v '||' w,y )
let a, b, c, d be Element of OAS; :: thesis: for u, v, w, y being VECTOR of V st a = u & b = v & c = w & d = y holds
( a,b '||' c,d iff u,v '||' w,y )
let u, v, w, y be VECTOR of V; :: thesis: ( a = u & b = v & c = w & d = y implies ( a,b '||' c,d iff u,v '||' w,y ) )
assume A2: ( a = u & b = v & c = w & d = y ) ; :: thesis: ( a,b '||' c,d iff u,v '||' w,y )
A3: now :: thesis: ( u,v '||' w,y implies a,b '||' c,d )
assume u,v '||' w,y ; :: thesis: a,b '||' c,d
then ( u,v // w,y or u,v // y,w ) by GEOMTRAP:def 1;
then ( a,b // c,d or a,b // d,c ) by A1, A2, GEOMTRAP:2;
hence a,b '||' c,d by DIRAF:def 4; :: thesis: verum
end;
now :: thesis: ( a,b '||' c,d implies u,v '||' w,y )
assume a,b '||' c,d ; :: thesis: u,v '||' w,y
then ( a,b // c,d or a,b // d,c ) by DIRAF:def 4;
then ( u,v // w,y or u,v // y,w ) by A1, A2, GEOMTRAP:2;
hence u,v '||' w,y by GEOMTRAP:def 1; :: thesis: verum
end;
hence ( a,b '||' c,d iff u,v '||' w,y ) by A3; :: thesis: verum