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