let R be non empty RelStr ; :: thesis: ( R is reflexive implies Flip (f_0 R) cc= id (bool the carrier of R) )
assume A0: R is reflexive ; :: thesis: Flip (f_0 R) cc= id (bool the carrier of R)
Flip (f_0 R) = LAp R by FlipLAp;
hence Flip (f_0 R) cc= id (bool the carrier of R) by A0, LApId; :: thesis: verum