let R be non empty RelStr ; :: thesis: Flip (UAp R) = LAp R
set f = Flip (UAp R);
set g = LAp R;
for x being Subset of R holds (Flip (UAp R)) . x = (LAp R) . x
proof
let x be Subset of R; :: thesis: (Flip (UAp R)) . x = (LAp R) . x
(Flip (UAp R)) . x = ((UAp R) . (x `)) ` by Def14
.= Lap x by Def11
.= LAp x by Th9
.= (LAp R) . x by Def10 ;
hence (Flip (UAp R)) . x = (LAp R) . x ; :: thesis: verum
end;
hence Flip (UAp R) = LAp R ; :: thesis: verum