:: deftheorem CompDef defines pcs-Compatible LATWAL_2:def 1 :
for P being pcs-Str holds
( P is pcs-Compatible iff for a1, a2, b1, b2 being Element of P st a1 (--) b1 & a2 (--) b2 holds
( a1 "\/" a2 (--) b1 "\/" b2 & a1 "/\" a2 (--) b1 "/\" b2 ) );