theorem Th6: :: PCS_0:6

for S1, S2 being non empty TolStr
for a, c being Element of S1
for b, d being Element of S2 holds
( [^a,b^] (--) [^c,d^] iff ( a (--) c or b (--) d ) ) by Def3;