Theorem T000713

The converse ( ) follows from these theorems:

Id If Then
T56
T214
T712
T648