let D be non empty set ; :: thesis: Top (PartialPredConnectivesLatt D) = PP_True D
set L = PartialPredConnectivesLatt D;
reconsider f = PP_True 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_or ((PP_True D),a1) by Def12
.= f by Th45 ; :: thesis: a "\/" f = f
hence a "\/" f = f ; :: thesis: verum
end;
hence Top (PartialPredConnectivesLatt D) = PP_True D by LATTICES:def 17; :: thesis: verum