set L = PartialPredConnectivesLatt D;
thus PartialPredConnectivesLatt D is lower-bounded :: according to LATTICES:def 15 :: thesis: PartialPredConnectivesLatt D is upper-bounded
proof
set c1 = PP_False D;
reconsider c = PP_False D as Element of (PartialPredConnectivesLatt D) by PARTFUN1:45;
take c ; :: according to LATTICES:def 13 :: thesis: for b1 being Element of the carrier of (PartialPredConnectivesLatt D) holds
( c "/\" b1 = c & b1 "/\" c = c )
let a be Element of (PartialPredConnectivesLatt D); :: thesis: ( c "/\" a = c & a "/\" c = c )
reconsider a1 = a as PartialPredicate of D by PARTFUN1:46;
thus c "/\" a = PP_and ((PP_False D),a1) by Def11
.= c by Th47 ; :: thesis: a "/\" c = c
thus a "/\" c = PP_and (a1,(PP_False D)) by Def11
.= c by Th47 ; :: thesis: verum
end;
thus PartialPredConnectivesLatt D is upper-bounded :: thesis: verum
proof
set c1 = PP_True D;
reconsider c = PP_True D as Element of (PartialPredConnectivesLatt D) by PARTFUN1:45;
take c ; :: according to LATTICES:def 14 :: thesis: for b1 being Element of the carrier of (PartialPredConnectivesLatt D) holds
( c "\/" b1 = c & b1 "\/" c = c )
let a be Element of (PartialPredConnectivesLatt D); :: thesis: ( c "\/" a = c & a "\/" c = c )
reconsider a1 = a as PartialPredicate of D by PARTFUN1:46;
thus c "\/" a = PP_or ((PP_True D),a1) by Def12
.= c by Th45 ; :: thesis: a "\/" c = c
thus a "\/" c = PP_or (a1,(PP_True D)) by Def12
.= c by Th45 ; :: thesis: verum
end;