let D be non empty set ; :: thesis: Bottom (PartialPredConnectivesLatt D) = PP_False D
set L = PartialPredConnectivesLatt D;
reconsider f = PP_False D as Element of (PartialPredConnectivesLatt D) by PARTFUN1:45;
for a being Element of (PartialPredConnectivesLatt D) holds
( f "/\" a = f & a "/\" f = f )
proof
let a be Element of (PartialPredConnectivesLatt D); :: thesis: ( f "/\" a = f & a "/\" f = f )
reconsider a1 = a as PartialPredicate of D by PARTFUN1:46;
thus f "/\" a = PP_and ((PP_False D),a1) by Def11
.= f by Th47 ; :: thesis: a "/\" f = f
hence a "/\" f = f ; :: thesis: verum
end;
hence Bottom (PartialPredConnectivesLatt D) = PP_False D by LATTICES:def 16; :: thesis: verum