let D be set ; :: thesis: PP_not (PP_False D) = PP_True D
set T = PP_True D;
set B = PP_False D;
set n = PP_not (PP_False D);
A1: dom (PP_False D) = D ;
hence dom (PP_not (PP_False D)) = dom (PP_True D) by Def2; :: according to FUNCT_1:def 11 :: thesis: for b₁ being object holds
( not b₁ in dom (PP_not (PP_False D)) or (PP_not (PP_False D)) . b₁ = (PP_True D) . b₁ )
let x be object ; :: thesis: ( not x in dom (PP_not (PP_False D)) or (PP_not (PP_False D)) . x = (PP_True D) . x )
assume A2: x in dom (PP_not (PP_False D)) ; :: thesis: (PP_not (PP_False D)) . x = (PP_True D) . x
then (PP_False D) . x = FALSE by FUNCOP_1:7;
hence (PP_not (PP_False D)) . x = TRUE by A1, A2, Def2
.= (PP_True D) . x by A2, FUNCOP_1:7 ;
:: thesis: verum