let X be set ; :: thesis: bool X <> X
X in bool X by Def1;
hence bool X <> X ; :: thesis: verum