let p, q, r be Element of CQC-WFF ; :: thesis: ( p,q are_similar & q,r are_similar implies p,r are_similar )
assume that
A1: p,q are_similar and
A2: q,r are_similar ; :: thesis: p,r are_similar
A3: SepVar q = SepVar r by A2, Def14;
SepVar p = SepVar q by A1, Def14;
hence p,r are_similar by A3, Def14; :: thesis: verum