A1: [:a,b:] c= [:a,b:] ;
thus not for b₁ being Relation of a,b holds b₁ is empty by A1; :: thesis: verum