:: deftheorem defines satisfying_OSCH CONMETR:def 7 :
for X being OrtAfPl holds
( X is satisfying_OSCH iff for a1, a2, a3, a4, b1, b2, b3, b4 being Element of X
for M, N being Subset of X st M _|_ N & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M & not b2 in M & not b4 in M & not a1 in N & not a3 in N & not b1 in N & not b3 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds
a3,a4 // b3,b4 );