let POS be OrtAfSp; :: thesis: for p, q, a, b, c, d being Element of 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 ; :: 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 p' = p, q' = q, a' = a, b' = b, c' = c, d' = d as Element of ;
( ( 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' ) ) by A2, Th48;
then a',b' // c',d' by A1, AFF_1:14;
hence a,b // c,d by Th48; :: thesis: verum