:: CONLAT_2 semantic presentation begin definitionlet "C" be ($#l1_conlat_1 :::"FormalContext":::); let "CP" be ($#v4_conlat_1 :::"strict"::: ) ($#l2_conlat_1 :::"FormalConcept":::) "of" (Set (Const "C")); func :::"@"::: "CP" -> ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k11_conlat_1 :::"ConceptLattice"::: ) "C" ")" ) equals :: CONLAT_2:def 1 "CP"; end; :: deftheorem defines :::"@"::: CONLAT_2:def 1 : (Bool "for" (Set (Var "C")) "being" ($#l1_conlat_1 :::"FormalContext":::) (Bool "for" (Set (Var "CP")) "being" ($#v4_conlat_1 :::"strict"::: ) ($#l2_conlat_1 :::"FormalConcept":::) "of" (Set (Var "C")) "holds" (Bool (Set ($#k1_conlat_2 :::"@"::: ) (Set (Var "CP"))) ($#r1_hidden :::"="::: ) (Set (Var "CP"))))); registrationlet "C" be ($#l1_conlat_1 :::"FormalContext":::); cluster (Set ($#k11_conlat_1 :::"ConceptLattice"::: ) "C") -> ($#v15_lattices :::"bounded"::: ) ; end; theorem :: CONLAT_2:1 (Bool "for" (Set (Var "C")) "being" ($#l1_conlat_1 :::"FormalContext":::) "holds" (Bool "(" (Bool (Set ($#k5_lattices :::"Bottom"::: ) (Set "(" ($#k11_conlat_1 :::"ConceptLattice"::: ) (Set (Var "C")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_conlat_1 :::"Concept-with-all-Attributes"::: ) (Set (Var "C")))) & (Bool (Set ($#k6_lattices :::"Top"::: ) (Set "(" ($#k11_conlat_1 :::"ConceptLattice"::: ) (Set (Var "C")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_conlat_1 :::"Concept-with-all-Objects"::: ) (Set (Var "C")))) ")" )) ; theorem :: CONLAT_2:2 (Bool "for" (Set (Var "C")) "being" ($#l1_conlat_1 :::"FormalContext":::) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C"))) "holds" (Bool (Set (Set "(" ($#k1_conlat_1 :::"ObjectDerivation"::: ) (Set (Var "C")) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k5_setfam_1 :::"union"::: ) (Set (Var "D")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) "{" (Set "(" (Set "(" ($#k1_conlat_1 :::"ObjectDerivation"::: ) (Set (Var "C")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "O")) ")" ) where O "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C"))) : (Bool (Set (Var "O")) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) "}" )))) ; theorem :: CONLAT_2:3 (Bool "for" (Set (Var "C")) "being" ($#l1_conlat_1 :::"FormalContext":::) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) "holds" (Bool (Set (Set "(" ($#k2_conlat_1 :::"AttributeDerivation"::: ) (Set (Var "C")) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k5_setfam_1 :::"union"::: ) (Set (Var "D")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) "{" (Set "(" (Set "(" ($#k2_conlat_1 :::"AttributeDerivation"::: ) (Set (Var "C")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "A")) ")" ) where A "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) : (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) "}" )))) ; theorem :: CONLAT_2:4 (Bool "for" (Set (Var "C")) "being" ($#l1_conlat_1 :::"FormalContext":::) (Bool "for" (Set (Var "D")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_conlat_1 :::"ConceptLattice"::: ) (Set (Var "C")) ")" ) "holds" (Bool "(" (Bool (Set ($#k16_lattice3 :::""/\""::: ) "(" (Set (Var "D")) "," (Set "(" ($#k11_conlat_1 :::"ConceptLattice"::: ) (Set (Var "C")) ")" ) ")" ) "is" ($#l2_conlat_1 :::"FormalConcept":::) "of" (Set (Var "C"))) & (Bool (Set ($#k15_lattice3 :::""\/""::: ) "(" (Set (Var "D")) "," (Set "(" ($#k11_conlat_1 :::"ConceptLattice"::: ) (Set (Var "C")) ")" ) ")" ) "is" ($#l2_conlat_1 :::"FormalConcept":::) "of" (Set (Var "C"))) ")" ))) ; definitionlet "C" be ($#l1_conlat_1 :::"FormalContext":::); let "D" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_conlat_1 :::"ConceptLattice"::: ) (Set (Const "C")) ")" ); func :::""/\""::: "(" "D" "," "C" ")" -> ($#l2_conlat_1 :::"FormalConcept":::) "of" "C" equals :: CONLAT_2:def 2 (Set ($#k16_lattice3 :::""/\""::: ) "(" "D" "," (Set "(" ($#k11_conlat_1 :::"ConceptLattice"::: ) "C" ")" ) ")" ); func :::""\/""::: "(" "D" "," "C" ")" -> ($#l2_conlat_1 :::"FormalConcept":::) "of" "C" equals :: CONLAT_2:def 3 (Set ($#k15_lattice3 :::""\/""::: ) "(" "D" "," (Set "(" ($#k11_conlat_1 :::"ConceptLattice"::: ) "C" ")" ) ")" ); end; :: deftheorem defines :::""/\""::: CONLAT_2:def 2 : (Bool "for" (Set (Var "C")) "being" ($#l1_conlat_1 :::"FormalContext":::) (Bool "for" (Set (Var "D")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_conlat_1 :::"ConceptLattice"::: ) (Set (Var "C")) ")" ) "holds" (Bool (Set ($#k2_conlat_2 :::""/\""::: ) "(" (Set (Var "D")) "," (Set (Var "C")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k16_lattice3 :::""/\""::: ) "(" (Set (Var "D")) "," (Set "(" ($#k11_conlat_1 :::"ConceptLattice"::: ) (Set (Var "C")) ")" ) ")" )))); :: deftheorem defines :::""\/""::: CONLAT_2:def 3 : (Bool "for" (Set (Var "C")) "being" ($#l1_conlat_1 :::"FormalContext":::) (Bool "for" (Set (Var "D")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_conlat_1 :::"ConceptLattice"::: ) (Set (Var "C")) ")" ) "holds" (Bool (Set ($#k3_conlat_2 :::""\/""::: ) "(" (Set (Var "D")) "," (Set (Var "C")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k15_lattice3 :::""\/""::: ) "(" (Set (Var "D")) "," (Set "(" ($#k11_conlat_1 :::"ConceptLattice"::: ) (Set (Var "C")) ")" ) ")" )))); theorem :: CONLAT_2:5 (Bool "for" (Set (Var "C")) "being" ($#l1_conlat_1 :::"FormalContext":::) "holds" (Bool "(" (Bool (Set ($#k3_conlat_2 :::""\/""::: ) "(" (Set "(" ($#k1_struct_0 :::"{}"::: ) (Set "(" ($#k11_conlat_1 :::"ConceptLattice"::: ) (Set (Var "C")) ")" ) ")" ) "," (Set (Var "C")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_conlat_1 :::"Concept-with-all-Attributes"::: ) (Set (Var "C")))) & (Bool (Set ($#k2_conlat_2 :::""/\""::: ) "(" (Set "(" ($#k1_struct_0 :::"{}"::: ) (Set "(" ($#k11_conlat_1 :::"ConceptLattice"::: ) (Set (Var "C")) ")" ) ")" ) "," (Set (Var "C")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_conlat_1 :::"Concept-with-all-Objects"::: ) (Set (Var "C")))) ")" )) ; theorem :: CONLAT_2:6 (Bool "for" (Set (Var "C")) "being" ($#l1_conlat_1 :::"FormalContext":::) "holds" (Bool "(" (Bool (Set ($#k3_conlat_2 :::""\/""::: ) "(" (Set "(" ($#k2_subset_1 :::"[#]"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k11_conlat_1 :::"ConceptLattice"::: ) (Set (Var "C")) ")" )) ")" ) "," (Set (Var "C")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_conlat_1 :::"Concept-with-all-Objects"::: ) (Set (Var "C")))) & (Bool (Set ($#k2_conlat_2 :::""/\""::: ) "(" (Set "(" ($#k2_subset_1 :::"[#]"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k11_conlat_1 :::"ConceptLattice"::: ) (Set (Var "C")) ")" )) ")" ) "," (Set (Var "C")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_conlat_1 :::"Concept-with-all-Attributes"::: ) (Set (Var "C")))) ")" )) ; theorem :: CONLAT_2:7 (Bool "for" (Set (Var "C")) "being" ($#l1_conlat_1 :::"FormalContext":::) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_conlat_1 :::"ConceptLattice"::: ) (Set (Var "C")) ")" ) "holds" (Bool "(" (Bool (Set "the" ($#u2_conlat_1 :::"Extent"::: ) "of" (Set "(" ($#k3_conlat_2 :::""\/""::: ) "(" (Set (Var "D")) "," (Set (Var "C")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_conlat_1 :::"AttributeDerivation"::: ) (Set (Var "C")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k1_conlat_1 :::"ObjectDerivation"::: ) (Set (Var "C")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_tarski :::"union"::: ) "{" (Set "the" ($#u2_conlat_1 :::"Extent"::: ) "of" (Set ($#g2_conlat_1 :::"ConceptStr"::: ) "(#" (Set (Var "E")) "," (Set (Var "I")) "#)" )) where E "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C"))), I "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) : (Bool (Set ($#g2_conlat_1 :::"ConceptStr"::: ) "(#" (Set (Var "E")) "," (Set (Var "I")) "#)" ) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) "}" ")" ) ")" ))) & (Bool (Set "the" ($#u3_conlat_1 :::"Intent"::: ) "of" (Set "(" ($#k3_conlat_2 :::""\/""::: ) "(" (Set (Var "D")) "," (Set (Var "C")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) "{" (Set "the" ($#u3_conlat_1 :::"Intent"::: ) "of" (Set ($#g2_conlat_1 :::"ConceptStr"::: ) "(#" (Set (Var "E")) "," (Set (Var "I")) "#)" )) where E "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C"))), I "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) : (Bool (Set ($#g2_conlat_1 :::"ConceptStr"::: ) "(#" (Set (Var "E")) "," (Set (Var "I")) "#)" ) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) "}" )) ")" ))) ; theorem :: CONLAT_2:8 (Bool "for" (Set (Var "C")) "being" ($#l1_conlat_1 :::"FormalContext":::) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_conlat_1 :::"ConceptLattice"::: ) (Set (Var "C")) ")" ) "holds" (Bool "(" (Bool (Set "the" ($#u2_conlat_1 :::"Extent"::: ) "of" (Set "(" ($#k2_conlat_2 :::""/\""::: ) "(" (Set (Var "D")) "," (Set (Var "C")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) "{" (Set "the" ($#u2_conlat_1 :::"Extent"::: ) "of" (Set ($#g2_conlat_1 :::"ConceptStr"::: ) "(#" (Set (Var "E")) "," (Set (Var "I")) "#)" )) where E "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C"))), I "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) : (Bool (Set ($#g2_conlat_1 :::"ConceptStr"::: ) "(#" (Set (Var "E")) "," (Set (Var "I")) "#)" ) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) "}" )) & (Bool (Set "the" ($#u3_conlat_1 :::"Intent"::: ) "of" (Set "(" ($#k2_conlat_2 :::""/\""::: ) "(" (Set (Var "D")) "," (Set (Var "C")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_conlat_1 :::"ObjectDerivation"::: ) (Set (Var "C")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k2_conlat_1 :::"AttributeDerivation"::: ) (Set (Var "C")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_tarski :::"union"::: ) "{" (Set "the" ($#u3_conlat_1 :::"Intent"::: ) "of" (Set ($#g2_conlat_1 :::"ConceptStr"::: ) "(#" (Set (Var "E")) "," (Set (Var "I")) "#)" )) where E "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C"))), I "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) : (Bool (Set ($#g2_conlat_1 :::"ConceptStr"::: ) "(#" (Set (Var "E")) "," (Set (Var "I")) "#)" ) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) "}" ")" ) ")" ))) ")" ))) ; theorem :: CONLAT_2:9 (Bool "for" (Set (Var "C")) "being" ($#l1_conlat_1 :::"FormalContext":::) (Bool "for" (Set (Var "CP")) "being" ($#v4_conlat_1 :::"strict"::: ) ($#l2_conlat_1 :::"FormalConcept":::) "of" (Set (Var "C")) "holds" (Bool (Set ($#k15_lattice3 :::""\/""::: ) "(" "{" (Set ($#g2_conlat_1 :::"ConceptStr"::: ) "(#" (Set (Var "O")) "," (Set (Var "A")) "#)" ) where O "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C"))), A "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) : (Bool "ex" (Set (Var "o")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "st" (Bool "(" (Bool (Set (Var "o")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u2_conlat_1 :::"Extent"::: ) "of" (Set (Var "CP")))) & (Bool (Set (Var "O")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_conlat_1 :::"AttributeDerivation"::: ) (Set (Var "C")) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set "(" ($#k1_conlat_1 :::"ObjectDerivation"::: ) (Set (Var "C")) ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "o")) ($#k6_domain_1 :::"}"::: ) ) ")" ))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_conlat_1 :::"ObjectDerivation"::: ) (Set (Var "C")) ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "o")) ($#k6_domain_1 :::"}"::: ) ))) ")" )) "}" "," (Set "(" ($#k11_conlat_1 :::"ConceptLattice"::: ) (Set (Var "C")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "CP"))))) ; theorem :: CONLAT_2:10 (Bool "for" (Set (Var "C")) "being" ($#l1_conlat_1 :::"FormalContext":::) (Bool "for" (Set (Var "CP")) "being" ($#v4_conlat_1 :::"strict"::: ) ($#l2_conlat_1 :::"FormalConcept":::) "of" (Set (Var "C")) "holds" (Bool (Set ($#k16_lattice3 :::""/\""::: ) "(" "{" (Set ($#g2_conlat_1 :::"ConceptStr"::: ) "(#" (Set (Var "O")) "," (Set (Var "A")) "#)" ) where O "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C"))), A "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) : (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Attribute":::) "of" (Set (Var "C")) "st" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u3_conlat_1 :::"Intent"::: ) "of" (Set (Var "CP")))) & (Bool (Set (Var "O")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_conlat_1 :::"AttributeDerivation"::: ) (Set (Var "C")) ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "a")) ($#k6_domain_1 :::"}"::: ) ))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_conlat_1 :::"ObjectDerivation"::: ) (Set (Var "C")) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set "(" ($#k2_conlat_1 :::"AttributeDerivation"::: ) (Set (Var "C")) ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "a")) ($#k6_domain_1 :::"}"::: ) ) ")" ))) ")" )) "}" "," (Set "(" ($#k11_conlat_1 :::"ConceptLattice"::: ) (Set (Var "C")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "CP"))))) ; definitionlet "C" be ($#l1_conlat_1 :::"FormalContext":::); func :::"gamma"::: "C" -> ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "C") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k11_conlat_1 :::"ConceptLattice"::: ) "C" ")" )) means :: CONLAT_2:def 4 (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Element":::) "of" "C" (Bool "ex" (Set (Var "O")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "C")(Bool "ex" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "C") "st" (Bool "(" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "o"))) ($#r1_hidden :::"="::: ) (Set ($#g2_conlat_1 :::"ConceptStr"::: ) "(#" (Set (Var "O")) "," (Set (Var "A")) "#)" )) & (Bool (Set (Var "O")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_conlat_1 :::"AttributeDerivation"::: ) "C" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set "(" ($#k1_conlat_1 :::"ObjectDerivation"::: ) "C" ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "o")) ($#k6_domain_1 :::"}"::: ) ) ")" ))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_conlat_1 :::"ObjectDerivation"::: ) "C" ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "o")) ($#k6_domain_1 :::"}"::: ) ))) ")" )))); end; :: deftheorem defines :::"gamma"::: CONLAT_2:def 4 : (Bool "for" (Set (Var "C")) "being" ($#l1_conlat_1 :::"FormalContext":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k11_conlat_1 :::"ConceptLattice"::: ) (Set (Var "C")) ")" )) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k4_conlat_2 :::"gamma"::: ) (Set (Var "C")))) "iff" (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "C")) (Bool "ex" (Set (Var "O")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C")))(Bool "ex" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) "st" (Bool "(" (Bool (Set (Set (Var "b2")) ($#k3_funct_2 :::"."::: ) (Set (Var "o"))) ($#r1_hidden :::"="::: ) (Set ($#g2_conlat_1 :::"ConceptStr"::: ) "(#" (Set (Var "O")) "," (Set (Var "A")) "#)" )) & (Bool (Set (Var "O")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_conlat_1 :::"AttributeDerivation"::: ) (Set (Var "C")) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set "(" ($#k1_conlat_1 :::"ObjectDerivation"::: ) (Set (Var "C")) ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "o")) ($#k6_domain_1 :::"}"::: ) ) ")" ))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_conlat_1 :::"ObjectDerivation"::: ) (Set (Var "C")) ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "o")) ($#k6_domain_1 :::"}"::: ) ))) ")" )))) ")" ))); definitionlet "C" be ($#l1_conlat_1 :::"FormalContext":::); func :::"delta"::: "C" -> ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "C") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k11_conlat_1 :::"ConceptLattice"::: ) "C" ")" )) means :: CONLAT_2:def 5 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "C") (Bool "ex" (Set (Var "O")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "C")(Bool "ex" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "C") "st" (Bool "(" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#g2_conlat_1 :::"ConceptStr"::: ) "(#" (Set (Var "O")) "," (Set (Var "A")) "#)" )) & (Bool (Set (Var "O")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_conlat_1 :::"AttributeDerivation"::: ) "C" ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "a")) ($#k6_domain_1 :::"}"::: ) ))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_conlat_1 :::"ObjectDerivation"::: ) "C" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set "(" ($#k2_conlat_1 :::"AttributeDerivation"::: ) "C" ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "a")) ($#k6_domain_1 :::"}"::: ) ) ")" ))) ")" )))); end; :: deftheorem defines :::"delta"::: CONLAT_2:def 5 : (Bool "for" (Set (Var "C")) "being" ($#l1_conlat_1 :::"FormalContext":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k11_conlat_1 :::"ConceptLattice"::: ) (Set (Var "C")) ")" )) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k5_conlat_2 :::"delta"::: ) (Set (Var "C")))) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) (Bool "ex" (Set (Var "O")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C")))(Bool "ex" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) "st" (Bool "(" (Bool (Set (Set (Var "b2")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#g2_conlat_1 :::"ConceptStr"::: ) "(#" (Set (Var "O")) "," (Set (Var "A")) "#)" )) & (Bool (Set (Var "O")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_conlat_1 :::"AttributeDerivation"::: ) (Set (Var "C")) ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "a")) ($#k6_domain_1 :::"}"::: ) ))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_conlat_1 :::"ObjectDerivation"::: ) (Set (Var "C")) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set "(" ($#k2_conlat_1 :::"AttributeDerivation"::: ) (Set (Var "C")) ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "a")) ($#k6_domain_1 :::"}"::: ) ) ")" ))) ")" )))) ")" ))); theorem :: CONLAT_2:11 (Bool "for" (Set (Var "C")) "being" ($#l1_conlat_1 :::"FormalContext":::) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Attribute":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k4_conlat_2 :::"gamma"::: ) (Set (Var "C")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "o"))) "is" ($#l2_conlat_1 :::"FormalConcept":::) "of" (Set (Var "C"))) & (Bool (Set (Set "(" ($#k5_conlat_2 :::"delta"::: ) (Set (Var "C")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) "is" ($#l2_conlat_1 :::"FormalConcept":::) "of" (Set (Var "C"))) ")" )))) ; theorem :: CONLAT_2:12 (Bool "for" (Set (Var "C")) "being" ($#l1_conlat_1 :::"FormalContext":::) "holds" (Bool "(" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" ($#k4_conlat_2 :::"gamma"::: ) (Set (Var "C")) ")" )) "is" ($#v8_lattice6 :::"supremum-dense"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" ($#k5_conlat_2 :::"delta"::: ) (Set (Var "C")) ")" )) "is" ($#v9_lattice6 :::"infimum-dense"::: ) ) ")" )) ; theorem :: CONLAT_2:13 (Bool "for" (Set (Var "C")) "being" ($#l1_conlat_1 :::"FormalContext":::) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Attribute":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set (Var "o")) ($#r1_conlat_1 :::"is-connected-with"::: ) (Set (Var "a"))) "iff" (Bool (Set (Set "(" ($#k4_conlat_2 :::"gamma"::: ) (Set (Var "C")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "o"))) ($#r3_lattices :::"[="::: ) (Set (Set "(" ($#k5_conlat_2 :::"delta"::: ) (Set (Var "C")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "a")))) ")" )))) ; begin theorem :: CONLAT_2:14 (Bool "for" (Set (Var "L")) "being" ($#v4_lattice3 :::"complete"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "C")) "being" ($#l1_conlat_1 :::"FormalContext":::) "holds" (Bool "(" (Bool (Set ($#k11_conlat_1 :::"ConceptLattice"::: ) (Set (Var "C"))) "," (Set (Var "L")) ($#r1_filter_1 :::"are_isomorphic"::: ) ) "iff" (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L")))(Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "st" (Bool "(" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "g"))) "is" ($#v8_lattice6 :::"supremum-dense"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "d"))) "is" ($#v9_lattice6 :::"infimum-dense"::: ) ) & (Bool "(" "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Attribute":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set (Var "o")) ($#r1_conlat_1 :::"is-connected-with"::: ) (Set (Var "a"))) "iff" (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "o"))) ($#r3_lattices :::"[="::: ) (Set (Set (Var "d")) ($#k3_funct_2 :::"."::: ) (Set (Var "a")))) ")" )) ")" ) ")" ))) ")" ))) ; definitionlet "L" be ($#l3_lattices :::"Lattice":::); func :::"Context"::: "L" -> ($#~v1_conlat_1 "non" ($#v1_conlat_1 :::"quasi-empty"::: ) ) ($#v2_conlat_1 :::"strict"::: ) ($#l1_conlat_1 :::"ContextStr"::: ) equals :: CONLAT_2:def 6 (Set ($#g1_conlat_1 :::"ContextStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L") "," (Set "(" ($#k2_lattice3 :::"LattRel"::: ) "L" ")" ) "#)" ); end; :: deftheorem defines :::"Context"::: CONLAT_2:def 6 : (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) "holds" (Bool (Set ($#k6_conlat_2 :::"Context"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set ($#g1_conlat_1 :::"ContextStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "," (Set "(" ($#k2_lattice3 :::"LattRel"::: ) (Set (Var "L")) ")" ) "#)" ))); theorem :: CONLAT_2:15 (Bool "for" (Set (Var "L")) "being" ($#v4_lattice3 :::"complete"::: ) ($#l3_lattices :::"Lattice":::) "holds" (Bool (Set ($#k11_conlat_1 :::"ConceptLattice"::: ) (Set "(" ($#k6_conlat_2 :::"Context"::: ) (Set (Var "L")) ")" )) "," (Set (Var "L")) ($#r1_filter_1 :::"are_isomorphic"::: ) )) ; theorem :: CONLAT_2:16 (Bool "for" (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v4_lattice3 :::"complete"::: ) ) "iff" (Bool "ex" (Set (Var "C")) "being" ($#l1_conlat_1 :::"FormalContext":::) "st" (Bool (Set ($#k11_conlat_1 :::"ConceptLattice"::: ) (Set (Var "C"))) "," (Set (Var "L")) ($#r1_filter_1 :::"are_isomorphic"::: ) )) ")" )) ; begin registrationlet "L" be ($#v4_lattice3 :::"complete"::: ) ($#l3_lattices :::"Lattice":::); cluster (Set "L" ($#k1_lattice2 :::".:"::: ) ) -> ($#v4_lattice3 :::"complete"::: ) ; end; definitionlet "C" be ($#l1_conlat_1 :::"FormalContext":::); func "C" :::".:"::: -> ($#~v1_conlat_1 "non" ($#v1_conlat_1 :::"quasi-empty"::: ) ) ($#v2_conlat_1 :::"strict"::: ) ($#l1_conlat_1 :::"ContextStr"::: ) equals :: CONLAT_2:def 7 (Set ($#g1_conlat_1 :::"ContextStr"::: ) "(#" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "C") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "C") "," (Set "(" (Set "the" ($#u1_conlat_1 :::"Information"::: ) "of" "C") ($#k3_relset_1 :::"~"::: ) ")" ) "#)" ); end; :: deftheorem defines :::".:"::: CONLAT_2:def 7 : (Bool "for" (Set (Var "C")) "being" ($#l1_conlat_1 :::"FormalContext":::) "holds" (Bool (Set (Set (Var "C")) ($#k7_conlat_2 :::".:"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#g1_conlat_1 :::"ContextStr"::: ) "(#" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C"))) "," (Set "(" (Set "the" ($#u1_conlat_1 :::"Information"::: ) "of" (Set (Var "C"))) ($#k3_relset_1 :::"~"::: ) ")" ) "#)" ))); theorem :: CONLAT_2:17 (Bool "for" (Set (Var "C")) "being" ($#v2_conlat_1 :::"strict"::: ) ($#l1_conlat_1 :::"FormalContext":::) "holds" (Bool (Set (Set "(" (Set (Var "C")) ($#k7_conlat_2 :::".:"::: ) ")" ) ($#k7_conlat_2 :::".:"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "C")))) ; theorem :: CONLAT_2:18 (Bool "for" (Set (Var "C")) "being" ($#l1_conlat_1 :::"FormalContext":::) (Bool "for" (Set (Var "O")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C"))) "holds" (Bool (Set (Set "(" ($#k1_conlat_1 :::"ObjectDerivation"::: ) (Set (Var "C")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "O"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_conlat_1 :::"AttributeDerivation"::: ) (Set "(" (Set (Var "C")) ($#k7_conlat_2 :::".:"::: ) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "O")))))) ; theorem :: CONLAT_2:19 (Bool "for" (Set (Var "C")) "being" ($#l1_conlat_1 :::"FormalContext":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) "holds" (Bool (Set (Set "(" ($#k2_conlat_1 :::"AttributeDerivation"::: ) (Set (Var "C")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_conlat_1 :::"ObjectDerivation"::: ) (Set "(" (Set (Var "C")) ($#k7_conlat_2 :::".:"::: ) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "A")))))) ; definitionlet "C" be ($#l1_conlat_1 :::"FormalContext":::); let "CP" be ($#l2_conlat_1 :::"ConceptStr"::: ) "over" (Set (Const "C")); func "CP" :::".:"::: -> ($#v4_conlat_1 :::"strict"::: ) ($#l2_conlat_1 :::"ConceptStr"::: ) "over" (Set "C" ($#k7_conlat_2 :::".:"::: ) ) means :: CONLAT_2:def 8 (Bool "(" (Bool (Set "the" ($#u2_conlat_1 :::"Extent"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set "the" ($#u3_conlat_1 :::"Intent"::: ) "of" "CP")) & (Bool (Set "the" ($#u3_conlat_1 :::"Intent"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set "the" ($#u2_conlat_1 :::"Extent"::: ) "of" "CP")) ")" ); end; :: deftheorem defines :::".:"::: CONLAT_2:def 8 : (Bool "for" (Set (Var "C")) "being" ($#l1_conlat_1 :::"FormalContext":::) (Bool "for" (Set (Var "CP")) "being" ($#l2_conlat_1 :::"ConceptStr"::: ) "over" (Set (Var "C")) (Bool "for" (Set (Var "b3")) "being" ($#v4_conlat_1 :::"strict"::: ) ($#l2_conlat_1 :::"ConceptStr"::: ) "over" (Set (Set (Var "C")) ($#k7_conlat_2 :::".:"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "CP")) ($#k8_conlat_2 :::".:"::: ) )) "iff" (Bool "(" (Bool (Set "the" ($#u2_conlat_1 :::"Extent"::: ) "of" (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u3_conlat_1 :::"Intent"::: ) "of" (Set (Var "CP")))) & (Bool (Set "the" ($#u3_conlat_1 :::"Intent"::: ) "of" (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u2_conlat_1 :::"Extent"::: ) "of" (Set (Var "CP")))) ")" ) ")" )))); registrationlet "C" be ($#l1_conlat_1 :::"FormalContext":::); let "CP" be ($#l2_conlat_1 :::"FormalConcept":::) "of" (Set (Const "C")); cluster (Set "CP" ($#k8_conlat_2 :::".:"::: ) ) -> ($#v4_conlat_1 :::"strict"::: ) ($#~v5_conlat_1 "non" ($#v5_conlat_1 :::"empty"::: ) ) ($#v7_conlat_1 :::"concept-like"::: ) ; end; theorem :: CONLAT_2:20 (Bool "for" (Set (Var "C")) "being" ($#v2_conlat_1 :::"strict"::: ) ($#l1_conlat_1 :::"FormalContext":::) (Bool "for" (Set (Var "CP")) "being" ($#v4_conlat_1 :::"strict"::: ) ($#l2_conlat_1 :::"FormalConcept":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set "(" (Set (Var "CP")) ($#k8_conlat_2 :::".:"::: ) ")" ) ($#k8_conlat_2 :::".:"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "CP"))))) ; definitionlet "C" be ($#l1_conlat_1 :::"FormalContext":::); func :::"DualHomomorphism"::: "C" -> ($#m1_lattice4 :::"Homomorphism"::: ) "of" (Set (Set "(" ($#k11_conlat_1 :::"ConceptLattice"::: ) "C" ")" ) ($#k1_lattice2 :::".:"::: ) ) "," (Set ($#k11_conlat_1 :::"ConceptLattice"::: ) (Set "(" "C" ($#k7_conlat_2 :::".:"::: ) ")" )) means :: CONLAT_2:def 9 (Bool "for" (Set (Var "CP")) "being" ($#v4_conlat_1 :::"strict"::: ) ($#l2_conlat_1 :::"FormalConcept":::) "of" "C" "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "CP"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "CP")) ($#k8_conlat_2 :::".:"::: ) ))); end; :: deftheorem defines :::"DualHomomorphism"::: CONLAT_2:def 9 : (Bool "for" (Set (Var "C")) "being" ($#l1_conlat_1 :::"FormalContext":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_lattice4 :::"Homomorphism"::: ) "of" (Set (Set "(" ($#k11_conlat_1 :::"ConceptLattice"::: ) (Set (Var "C")) ")" ) ($#k1_lattice2 :::".:"::: ) ) "," (Set ($#k11_conlat_1 :::"ConceptLattice"::: ) (Set "(" (Set (Var "C")) ($#k7_conlat_2 :::".:"::: ) ")" )) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k9_conlat_2 :::"DualHomomorphism"::: ) (Set (Var "C")))) "iff" (Bool "for" (Set (Var "CP")) "being" ($#v4_conlat_1 :::"strict"::: ) ($#l2_conlat_1 :::"FormalConcept":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "CP"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "CP")) ($#k8_conlat_2 :::".:"::: ) ))) ")" ))); theorem :: CONLAT_2:21 (Bool "for" (Set (Var "C")) "being" ($#l1_conlat_1 :::"FormalContext":::) "holds" (Bool (Set ($#k9_conlat_2 :::"DualHomomorphism"::: ) (Set (Var "C"))) "is" ($#v3_funct_2 :::"bijective"::: ) )) ; theorem :: CONLAT_2:22 (Bool "for" (Set (Var "C")) "being" ($#l1_conlat_1 :::"FormalContext":::) "holds" (Bool (Set ($#k11_conlat_1 :::"ConceptLattice"::: ) (Set "(" (Set (Var "C")) ($#k7_conlat_2 :::".:"::: ) ")" )) "," (Set (Set "(" ($#k11_conlat_1 :::"ConceptLattice"::: ) (Set (Var "C")) ")" ) ($#k1_lattice2 :::".:"::: ) ) ($#r1_filter_1 :::"are_isomorphic"::: ) )) ;