let V be RealLinearSpace; 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; ( 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
; 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; 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; ( 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 )
; ( a,b '||' c,d iff u,v '||' w,y )
A3:
now ( u,v '||' w,y implies a,b '||' c,d )assume
u,
v '||' w,
y
;
a,b '||' c,dthen
(
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;
verum end;
now ( a,b '||' c,d implies u,v '||' w,y )assume
a,
b '||' c,
d
;
u,v '||' w,ythen
(
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;
verum end;
hence
( a,b '||' c,d iff u,v '||' w,y )
by A3; verum