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