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 // c,d & p,q _|_ a,b ) or ( p,q // a,b & c,d _|_ p,q ) or ( p,q // c,d & a,b _|_ p,q ) or ( a,b // p,q & c,d _|_ p,q ) or ( c,d // p,q & a,b _|_ p,q ) or ( a,b // p,q & p,q _|_ c,d ) or ( c,d // p,q & p,q _|_ a,b ) ) 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 // c,d & p,q _|_ a,b ) or ( p,q // a,b & c,d _|_ p,q ) or ( p,q // c,d & a,b _|_ p,q ) or ( a,b // p,q & c,d _|_ p,q ) or ( c,d // p,q & a,b _|_ p,q ) or ( a,b // p,q & p,q _|_ c,d ) or ( c,d // p,q & p,q _|_ a,b ) ) implies a,b _|_ c,d )
assume that
A1: p <> q and
A2: ( ( p,q // a,b & p,q _|_ c,d ) or ( p,q // c,d & p,q _|_ a,b ) or ( p,q // a,b & c,d _|_ p,q ) or ( p,q // c,d & a,b _|_ p,q ) or ( a,b // p,q & c,d _|_ p,q ) or ( c,d // p,q & a,b _|_ p,q ) or ( a,b // p,q & p,q _|_ c,d ) or ( c,d // p,q & p,q _|_ a,b ) ) ; :: thesis: a,b _|_ c,d

A3: now :: thesis: ( ( ( 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 ( ( 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
then ( p,q // a,b & p,q _|_ c,d ) by Th59, Th61;
then c,d _|_ a,b by A1, Def7;
hence a,b _|_ c,d by Th61; :: thesis: verum

end;

now :: thesis: ( ( ( p,q // c,d & p,q _|_ a,b ) or ( p,q // c,d & a,b _|_ p,q ) or ( c,d // p,q & a,b _|_ p,q ) or ( c,d // p,q & p,q _|_ a,b ) ) implies a,b _|_ c,d )

assume ( ( p,q // c,d & p,q _|_ a,b ) or ( p,q // c,d & a,b _|_ p,q ) or ( c,d // p,q & a,b _|_ p,q ) or ( c,d // p,q & p,q _|_ a,b ) ) ; :: thesis: a,b _|_ c,d
then ( p,q // c,d & p,q _|_ a,b ) by Th59, Th61;
hence a,b _|_ c,d by A1, Def7; :: thesis: verum

end;

hence a,b _|_ c,d by A2, A3; :: thesis: verum