scheme :: ABSRED_0:sch 3
StarBack{ F₁() -> ARS , P₁[ object ] } :

for x, y being Element of F₁() st x =*=> y & P₁[y] holds
P₁[x]

provided

A1: for x, y being Element of F₁() st x ==> y & P₁[y] holds
P₁[x]