consider B being Binding of OAF;
take Normalized B ; :: thesis: Normalized B is normalized
thus Normalized B is normalized ; :: thesis: verum