let X be set ; :: thesis: for f being Function of (bool X),(bool X) st f . {} = {} holds
(Flip f) . X = X
let f be Function of (bool X),(bool X); :: thesis: ( f . {} = {} implies (Flip f) . X = X )
assume A1: f . {} = {} ; :: thesis: (Flip f) . X = X
X c= X ;
then reconsider y = X as Subset of X ;
(Flip f) . y = (f . (y `)) ` by Def14
.= ({} X) ` by A1
.= y ;
hence (Flip f) . X = X ; :: thesis: verum