let POS be OrtAfPl; 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; ( 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 ) )
; a,b // c,d
( p,q _|_ a,b & p,q _|_ c,d )
by A2, Th61;
hence
a,b // c,d
by A1, Def8; verum