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