A1: {a,b} c= A ;
hence rng (a <-> b) c= A by LemS; :: according to RELAT_1:def 19 :: thesis: a <-> b is A -defined
thus dom (a <-> b) c= A by A1, LemS; :: according to RELAT_1:def 18 :: thesis: verum