set B = the Binding of OAF;
take Normalized the Binding of OAF ; :: thesis: Normalized the Binding of OAF is normalized
thus Normalized the Binding of OAF is normalized ; :: thesis: verum