let V be RealLinearSpace; :: thesis: for p, q, s, y being Element of V

for a, b being Real st not are_Prop p,q & y = a * q & a <> 0 & s = b * p & b <> 0 holds

not are_Prop s,y

let p, q, s, y be Element of V; :: thesis: for a, b being Real st not are_Prop p,q & y = a * q & a <> 0 & s = b * p & b <> 0 holds

not are_Prop s,y

let a, b be Real; :: thesis: ( not are_Prop p,q & y = a * q & a <> 0 & s = b * p & b <> 0 implies not are_Prop s,y )

assume that

A1: not are_Prop p,q and

A2: ( y = a * q & a <> 0 ) and

A3: ( s = b * p & b <> 0 ) ; :: thesis: not are_Prop s,y

assume are_Prop s,y ; :: thesis: contradiction

then consider c being Real such that

A4: ( c <> 0 & s = c * y ) by ANPROJ_1:1;

( s = (c * a) * q & c * a <> 0 ) by A2, A4, RLVECT_1:def 7, XCMPLX_1:6;

hence contradiction by A1, A3; :: thesis: verum

for a, b being Real st not are_Prop p,q & y = a * q & a <> 0 & s = b * p & b <> 0 holds

not are_Prop s,y

let p, q, s, y be Element of V; :: thesis: for a, b being Real st not are_Prop p,q & y = a * q & a <> 0 & s = b * p & b <> 0 holds

not are_Prop s,y

let a, b be Real; :: thesis: ( not are_Prop p,q & y = a * q & a <> 0 & s = b * p & b <> 0 implies not are_Prop s,y )

assume that

A1: not are_Prop p,q and

A2: ( y = a * q & a <> 0 ) and

A3: ( s = b * p & b <> 0 ) ; :: thesis: not are_Prop s,y

assume are_Prop s,y ; :: thesis: contradiction

then consider c being Real such that

A4: ( c <> 0 & s = c * y ) by ANPROJ_1:1;

( s = (c * a) * q & c * a <> 0 ) by A2, A4, RLVECT_1:def 7, XCMPLX_1:6;

hence contradiction by A1, A3; :: thesis: verum