let D be non empty set ; :: thesis: PP_or ((PP_BottomPred D),(PP_True D)) = PP_True D
set B = PP_BottomPred D;
set T = PP_True D;
set o = PP_or ((PP_BottomPred D),(PP_True D));
A1: dom (PP_or ((PP_BottomPred D),(PP_True D))) = { d where d is Element of D : ( ( d in dom (PP_BottomPred D) & (PP_BottomPred D) . d = TRUE ) or ( d in dom (PP_True D) & (PP_True D) . d = TRUE ) or ( d in dom (PP_BottomPred D) & (PP_BottomPred D) . d = FALSE & d in dom (PP_True D) & (PP_True D) . d = FALSE ) ) } by Def4;
thus dom (PP_or ((PP_BottomPred D),(PP_True D))) = dom (PP_True D) :: according to FUNCT_1:def 11 :: thesis: for b₁ being object holds
( not b₁ in dom (PP_or ((PP_BottomPred D),(PP_True D))) or (PP_or ((PP_BottomPred D),(PP_True D))) . b₁ = (PP_True D) . b₁ )

proof

thus dom (PP_or ((PP_BottomPred D),(PP_True D))) c= dom (PP_True D) ; :: according to XBOOLE_0:def 10 :: thesis: dom (PP_True D) c= dom (PP_or ((PP_BottomPred D),(PP_True D)))
thus dom (PP_True D) c= dom (PP_or ((PP_BottomPred D),(PP_True D))) :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom (PP_True D) or x in dom (PP_or ((PP_BottomPred D),(PP_True D))) )
assume A2: x in dom (PP_True D) ; :: thesis: x in dom (PP_or ((PP_BottomPred D),(PP_True D)))
then (PP_True D) . x = TRUE by FUNCOP_1:7;
hence x in dom (PP_or ((PP_BottomPred D),(PP_True D))) by A1, A2; :: thesis: verum

end;

end;

let x be object ; :: thesis: ( not x in dom (PP_or ((PP_BottomPred D),(PP_True D))) or (PP_or ((PP_BottomPred D),(PP_True D))) . x = (PP_True D) . x )
assume x in dom (PP_or ((PP_BottomPred D),(PP_True D))) ; :: thesis: (PP_or ((PP_BottomPred D),(PP_True D))) . x = (PP_True D) . x

per cases then ( ( x in dom (PP_BottomPred D) & (PP_BottomPred D) . x = TRUE ) or ( x in dom (PP_BottomPred D) & (PP_BottomPred D) . x = FALSE & x in dom (PP_True D) & (PP_True D) . x = FALSE ) or ( x in dom (PP_True D) & (PP_True D) . x = TRUE ) ) by Th8;

suppose ( ( x in dom (PP_BottomPred D) & (PP_BottomPred D) . x = TRUE ) or ( x in dom (PP_BottomPred D) & (PP_BottomPred D) . x = FALSE & x in dom (PP_True D) & (PP_True D) . x = FALSE ) ) ; :: thesis: (PP_or ((PP_BottomPred D),(PP_True D))) . x = (PP_True D) . x

hence (PP_or ((PP_BottomPred D),(PP_True D))) . x = (PP_True D) . x ; :: thesis: verum

end;

suppose ( x in dom (PP_True D) & (PP_True D) . x = TRUE ) ; :: thesis: (PP_or ((PP_BottomPred D),(PP_True D))) . x = (PP_True D) . x

hence (PP_or ((PP_BottomPred D),(PP_True D))) . x = (PP_True D) . x by Def4; :: thesis: verum

end;

end;