let SAS be Semi_Affine_Space; :: thesis: for a, b, p, q, r, s being Element of SAS st a <> b & p,q // a,b & a,b // r,s holds
p,q // r,s
let a, b, p, q, r, s be Element of SAS; :: thesis: ( a <> b & p,q // a,b & a,b // r,s implies p,q // r,s )
assume that
A1: a <> b and
A2: p,q // a,b and
A3: a,b // r,s ; :: thesis: p,q // r,s
a,b // p,q by A2, Th6;
hence p,q // r,s by A1, A3, Def1; :: thesis: verum