set L = PartialPredConnectivesLatt D;
thus PartialPredConnectivesLatt D is join-commutative :: according to LATTICES:def 10 :: thesis: ( PartialPredConnectivesLatt D is join-associative & PartialPredConnectivesLatt D is meet-absorbing & PartialPredConnectivesLatt D is meet-commutative & PartialPredConnectivesLatt D is meet-associative & PartialPredConnectivesLatt D is join-absorbing )
proof
let a, b be Element of (PartialPredConnectivesLatt D); :: according to LATTICES:def 4 :: thesis: a "\/" b = b "\/" a
reconsider a1 = a, b1 = b as PartialPredicate of D by PARTFUN1:46;
thus a "\/" b = PP_or (b1,a1) by Def12
.= b "\/" a by Def12 ; :: thesis: verum
end;
thus PartialPredConnectivesLatt D is join-associative :: thesis: ( PartialPredConnectivesLatt D is meet-absorbing & PartialPredConnectivesLatt D is meet-commutative & PartialPredConnectivesLatt D is meet-associative & PartialPredConnectivesLatt D is join-absorbing )
proof
let a, b, c be Element of (PartialPredConnectivesLatt D); :: according to LATTICES:def 5 :: thesis: a "\/" (b "\/" c) = (a "\/" b) "\/" c
reconsider a1 = a, b1 = b, c1 = c as PartialPredicate of D by PARTFUN1:46;
A1: a "\/" b = PP_or (a1,b1) by Def12;
b "\/" c = PP_or (b1,c1) by Def12;
hence a "\/" (b "\/" c) = PP_or (a1,(PP_or (b1,c1))) by Def12
.= PP_or ((PP_or (a1,b1)),c1) by Th14
.= (a "\/" b) "\/" c by A1, Def12 ;
:: thesis: verum
end;
thus PartialPredConnectivesLatt D is meet-absorbing :: thesis: ( PartialPredConnectivesLatt D is meet-commutative & PartialPredConnectivesLatt D is meet-associative & PartialPredConnectivesLatt D is join-absorbing )
proof
let a, b be Element of (PartialPredConnectivesLatt D); :: according to LATTICES:def 8 :: thesis: (a "/\" b) "\/" b = b
reconsider a1 = a, b1 = b as PartialPredicate of D by PARTFUN1:46;
a "/\" b = PP_and (a1,b1) by Def11;
hence (a "/\" b) "\/" b = PP_or ((PP_and (a1,b1)),b1) by Def12
.= b by Th28 ;
:: thesis: verum
end;
thus PartialPredConnectivesLatt D is meet-commutative :: thesis: ( PartialPredConnectivesLatt D is meet-associative & PartialPredConnectivesLatt D is join-absorbing )
proof
let a, b be Element of (PartialPredConnectivesLatt D); :: according to LATTICES:def 6 :: thesis: a "/\" b = b "/\" a
reconsider a1 = a, b1 = b as PartialPredicate of D by PARTFUN1:46;
thus a "/\" b = PP_and (b1,a1) by Def11
.= b "/\" a by Def11 ; :: thesis: verum
end;
thus PartialPredConnectivesLatt D is meet-associative :: thesis: PartialPredConnectivesLatt D is join-absorbing
proof
let a, b, c be Element of (PartialPredConnectivesLatt D); :: according to LATTICES:def 7 :: thesis: a "/\" (b "/\" c) = (a "/\" b) "/\" c
reconsider a1 = a, b1 = b, c1 = c as PartialPredicate of D by PARTFUN1:46;
A2: a "/\" b = PP_and (a1,b1) by Def11;
b "/\" c = PP_and (b1,c1) by Def11;
hence a "/\" (b "/\" c) = PP_and (a1,(PP_and (b1,c1))) by Def11
.= PP_and ((PP_and (a1,b1)),c1) by Th14
.= (a "/\" b) "/\" c by A2, Def11 ;
:: thesis: verum
end;
thus PartialPredConnectivesLatt D is join-absorbing :: thesis: verum
proof
let a, b be Element of (PartialPredConnectivesLatt D); :: according to LATTICES:def 9 :: thesis: a "/\" (a "\/" b) = a
reconsider a1 = a, b1 = b as PartialPredicate of D by PARTFUN1:46;
a "\/" b = PP_or (a1,b1) by Def12;
hence a "/\" (a "\/" b) = PP_and (a1,(PP_or (a1,b1))) by Def11
.= a by Th29 ;
:: thesis: verum
end;