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

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