let POS be OrtAfSp; :: thesis: for a, b, c, d being Element of POS st a,b _|_ c,d holds
( a,b _|_ d,c & b,a _|_ c,d & b,a _|_ d,c & c,d _|_ a,b & c,d _|_ b,a & d,c _|_ a,b & d,c _|_ b,a )
let a, b, c, d be Element of POS; :: thesis: ( a,b _|_ c,d implies ( a,b _|_ d,c & b,a _|_ c,d & b,a _|_ d,c & c,d _|_ a,b & c,d _|_ b,a & d,c _|_ a,b & d,c _|_ b,a ) )
assume A1: a,b _|_ c,d ; :: thesis: ( a,b _|_ d,c & b,a _|_ c,d & b,a _|_ d,c & c,d _|_ a,b & c,d _|_ b,a & d,c _|_ a,b & d,c _|_ b,a )
then a,b _|_ d,c by Def7;
then A2: d,c _|_ a,b by Def7;
then d,c _|_ b,a by Def7;
then b,a _|_ d,c by Def7;
then b,a _|_ c,d by Def7;
hence ( a,b _|_ d,c & b,a _|_ c,d & b,a _|_ d,c & c,d _|_ a,b & c,d _|_ b,a & d,c _|_ a,b & d,c _|_ b,a ) by A1, A2, Def7; :: thesis: verum