let R be non empty RelStr ; :: thesis: Flip (LAp R) = UAp R
Flip (UAp R) = LAp R by Th27;
hence Flip (LAp R) = UAp R by Th23; :: thesis: verum