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 ( a <> b & p,q // a,b & a,b // r,s ) ; :: thesis: p,q // r,s
then ( a <> b & a,b // p,q & a,b // r,s ) by Th17;
hence p,q // r,s by Def1; :: thesis: verum