let R be non empty RelStr ; :: thesis: Flip (f_0 R) = LAp R
f_0 R = UAp R by UApF0;
hence Flip (f_0 R) = LAp R by ROUGHS_2:27; :: thesis: verum