let POS be OrtAfSp; :: thesis: for a, b, c, d, p, q being Element of POS st p <> q & ( ( p,q // a,b & p,q // c,d ) or ( p,q // a,b & c,d // p,q ) or ( a,b // p,q & c,d // p,q ) or ( a,b // p,q & p,q // c,d ) ) holds
a,b // c,d
let a, b, c, d, p, q be Element of POS; :: thesis: ( p <> q & ( ( p,q // a,b & p,q // c,d ) or ( p,q // a,b & c,d // p,q ) or ( a,b // p,q & c,d // p,q ) or ( a,b // p,q & p,q // c,d ) ) implies a,b // c,d )
assume that
A1: p <> q and
A2: ( ( p,q // a,b & p,q // c,d ) or ( p,q // a,b & c,d // p,q ) or ( a,b // p,q & c,d // p,q ) or ( a,b // p,q & p,q // c,d ) ) ; :: thesis: a,b // c,d
reconsider p9 = p, q9 = q, a9 = a, b9 = b, c9 = c, d9 = d as Element of AffinStruct(# the carrier of POS, the CONGR of POS #) ;
( ( p9,q9 // a9,b9 & p9,q9 // c9,d9 ) or ( p9,q9 // a9,b9 & c9,d9 // p9,q9 ) or ( a9,b9 // p9,q9 & c9,d9 // p9,q9 ) or ( a9,b9 // p9,q9 & p9,q9 // c9,d9 ) ) by A2, Th36;
then a9,b9 // c9,d9 by A1, AFF_1:5;
hence a,b // c,d by Th36; :: thesis: verum