let POS be OrtAfSp; :: thesis: for p, q, a, b, c, d 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 p, q, a, b, c, d 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 (Af 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, Th48;
then a9,b9 // c9,d9 by A1, AFF_1:14;
hence a,b // c,d by Th48; :: thesis: verum