:: FILTER_2 semantic presentation begin theorem Th1: :: FILTER_2:1 for D being non empty set for S being non empty Subset of D for f being BinOp of D for g being BinOp of S st g = f || S holds ( ( f is commutative implies g is commutative ) & ( f is idempotent implies g is idempotent ) & ( f is associative implies g is associative ) ) proof let D be non empty set ; ::_thesis: for S being non empty Subset of D for f being BinOp of D for g being BinOp of S st g = f || S holds ( ( f is commutative implies g is commutative ) & ( f is idempotent implies g is idempotent ) & ( f is associative implies g is associative ) ) let S be non empty Subset of D; ::_thesis: for f being BinOp of D for g being BinOp of S st g = f || S holds ( ( f is commutative implies g is commutative ) & ( f is idempotent implies g is idempotent ) & ( f is associative implies g is associative ) ) let f be BinOp of D; ::_thesis: for g being BinOp of S st g = f || S holds ( ( f is commutative implies g is commutative ) & ( f is idempotent implies g is idempotent ) & ( f is associative implies g is associative ) ) let g be BinOp of S; ::_thesis: ( g = f || S implies ( ( f is commutative implies g is commutative ) & ( f is idempotent implies g is idempotent ) & ( f is associative implies g is associative ) ) ) A1: dom g = [:S,S:] by FUNCT_2:def_1; assume A2: g = f || S ; ::_thesis: ( ( f is commutative implies g is commutative ) & ( f is idempotent implies g is idempotent ) & ( f is associative implies g is associative ) ) thus ( f is commutative implies g is commutative ) ::_thesis: ( ( f is idempotent implies g is idempotent ) & ( f is associative implies g is associative ) ) proof assume A3: for a, b being Element of D holds f . (a,b) = f . (b,a) ; :: according to BINOP_1:def_2 ::_thesis: g is commutative let a, b be Element of S; :: according to BINOP_1:def_2 ::_thesis: g . (a,b) = g . (b,a) reconsider a9 = a, b9 = b as Element of S ; reconsider a9 = a9, b9 = b9 as Element of D ; thus g . (a,b) = f . [a,b] by A2, A1, FUNCT_1:47 .= f . (a9,b9) .= f . (b9,a9) by A3 .= g . [b,a] by A2, A1, FUNCT_1:47 .= g . (b,a) ; ::_thesis: verum end; thus ( f is idempotent implies g is idempotent ) ::_thesis: ( f is associative implies g is associative ) proof assume A4: for a being Element of D holds f . (a,a) = a ; :: according to BINOP_1:def_4 ::_thesis: g is idempotent let a be Element of S; :: according to BINOP_1:def_4 ::_thesis: g . (a,a) = a thus g . (a,a) = f . [a,a] by A2, A1, FUNCT_1:47 .= f . (a,a) .= a by A4 ; ::_thesis: verum end; assume A5: for a, b, c being Element of D holds f . ((f . (a,b)),c) = f . (a,(f . (b,c))) ; :: according to BINOP_1:def_3 ::_thesis: g is associative let a, b, c be Element of S; :: according to BINOP_1:def_3 ::_thesis: g . (a,(g . (b,c))) = g . ((g . (a,b)),c) reconsider a9 = a, b9 = b, c9 = c as Element of S ; reconsider a9 = a9, b9 = b9, c9 = c9 as Element of D ; thus g . ((g . (a,b)),c) = f . [(g . (a,b)),c] by A2, A1, FUNCT_1:47 .= f . [(f . [a,b]),c] by A2, A1, FUNCT_1:47 .= f . ((f . (a,b)),c) .= f . (a9,(f . (b9,c9))) by A5 .= f . (a,(g . [b,c])) by A2, A1, FUNCT_1:47 .= f . [a,(g . (b,c))] .= g . (a,(g . (b,c))) by A2, A1, FUNCT_1:47 ; ::_thesis: verum end; theorem :: FILTER_2:2 for D being non empty set for S being non empty Subset of D for f being BinOp of D for g being BinOp of S for d being Element of D for d9 being Element of S st g = f || S & d9 = d holds ( ( d is_a_left_unity_wrt f implies d9 is_a_left_unity_wrt g ) & ( d is_a_right_unity_wrt f implies d9 is_a_right_unity_wrt g ) & ( d is_a_unity_wrt f implies d9 is_a_unity_wrt g ) ) proof let D be non empty set ; ::_thesis: for S being non empty Subset of D for f being BinOp of D for g being BinOp of S for d being Element of D for d9 being Element of S st g = f || S & d9 = d holds ( ( d is_a_left_unity_wrt f implies d9 is_a_left_unity_wrt g ) & ( d is_a_right_unity_wrt f implies d9 is_a_right_unity_wrt g ) & ( d is_a_unity_wrt f implies d9 is_a_unity_wrt g ) ) let S be non empty Subset of D; ::_thesis: for f being BinOp of D for g being BinOp of S for d being Element of D for d9 being Element of S st g = f || S & d9 = d holds ( ( d is_a_left_unity_wrt f implies d9 is_a_left_unity_wrt g ) & ( d is_a_right_unity_wrt f implies d9 is_a_right_unity_wrt g ) & ( d is_a_unity_wrt f implies d9 is_a_unity_wrt g ) ) let f be BinOp of D; ::_thesis: for g being BinOp of S for d being Element of D for d9 being Element of S st g = f || S & d9 = d holds ( ( d is_a_left_unity_wrt f implies d9 is_a_left_unity_wrt g ) & ( d is_a_right_unity_wrt f implies d9 is_a_right_unity_wrt g ) & ( d is_a_unity_wrt f implies d9 is_a_unity_wrt g ) ) let g be BinOp of S; ::_thesis: for d being Element of D for d9 being Element of S st g = f || S & d9 = d holds ( ( d is_a_left_unity_wrt f implies d9 is_a_left_unity_wrt g ) & ( d is_a_right_unity_wrt f implies d9 is_a_right_unity_wrt g ) & ( d is_a_unity_wrt f implies d9 is_a_unity_wrt g ) ) let d be Element of D; ::_thesis: for d9 being Element of S st g = f || S & d9 = d holds ( ( d is_a_left_unity_wrt f implies d9 is_a_left_unity_wrt g ) & ( d is_a_right_unity_wrt f implies d9 is_a_right_unity_wrt g ) & ( d is_a_unity_wrt f implies d9 is_a_unity_wrt g ) ) let d9 be Element of S; ::_thesis: ( g = f || S & d9 = d implies ( ( d is_a_left_unity_wrt f implies d9 is_a_left_unity_wrt g ) & ( d is_a_right_unity_wrt f implies d9 is_a_right_unity_wrt g ) & ( d is_a_unity_wrt f implies d9 is_a_unity_wrt g ) ) ) assume that A1: g = f || S and A2: d9 = d ; ::_thesis: ( ( d is_a_left_unity_wrt f implies d9 is_a_left_unity_wrt g ) & ( d is_a_right_unity_wrt f implies d9 is_a_right_unity_wrt g ) & ( d is_a_unity_wrt f implies d9 is_a_unity_wrt g ) ) A3: dom g = [:S,S:] by FUNCT_2:def_1; thus ( d is_a_left_unity_wrt f implies d9 is_a_left_unity_wrt g ) ::_thesis: ( ( d is_a_right_unity_wrt f implies d9 is_a_right_unity_wrt g ) & ( d is_a_unity_wrt f implies d9 is_a_unity_wrt g ) ) proof assume A4: for a being Element of D holds f . (d,a) = a ; :: according to BINOP_1:def_16 ::_thesis: d9 is_a_left_unity_wrt g let a be Element of S; :: according to BINOP_1:def_16 ::_thesis: g . (d9,a) = a thus g . (d9,a) = f . [d9,a] by A1, A3, FUNCT_1:47 .= f . (d,a) by A2 .= a by A4 ; ::_thesis: verum end; thus ( d is_a_right_unity_wrt f implies d9 is_a_right_unity_wrt g ) ::_thesis: ( d is_a_unity_wrt f implies d9 is_a_unity_wrt g ) proof assume A5: for a being Element of D holds f . (a,d) = a ; :: according to BINOP_1:def_17 ::_thesis: d9 is_a_right_unity_wrt g let a be Element of S; :: according to BINOP_1:def_17 ::_thesis: g . (a,d9) = a thus g . (a,d9) = f . [a,d9] by A1, A3, FUNCT_1:47 .= f . (a,d) by A2 .= a by A5 ; ::_thesis: verum end; assume A6: d is_a_unity_wrt f ; ::_thesis: d9 is_a_unity_wrt g now__::_thesis:_for_s_being_Element_of_S_holds_ (_g_._(d9,s)_=_s_&_g_._(s,d9)_=_s_) let s be Element of S; ::_thesis: ( g . (d9,s) = s & g . (s,d9) = s ) reconsider s9 = s as Element of D ; A7: dom g = [:S,S:] by FUNCT_2:def_1; [d9,s] in [:S,S:] ; hence g . (d9,s) = f . (d,s9) by A1, A2, A7, FUNCT_1:47 .= s by A6, BINOP_1:3 ; ::_thesis: g . (s,d9) = s [s,d9] in [:S,S:] ; hence g . (s,d9) = f . (s9,d) by A1, A2, A7, FUNCT_1:47 .= s by A6, BINOP_1:3 ; ::_thesis: verum end; hence d9 is_a_unity_wrt g by BINOP_1:3; ::_thesis: verum end; theorem Th3: :: FILTER_2:3 for D being non empty set for S being non empty Subset of D for f1, f2 being BinOp of D for g1, g2 being BinOp of S st g1 = f1 || S & g2 = f2 || S holds ( ( f1 is_left_distributive_wrt f2 implies g1 is_left_distributive_wrt g2 ) & ( f1 is_right_distributive_wrt f2 implies g1 is_right_distributive_wrt g2 ) ) proof let D be non empty set ; ::_thesis: for S being non empty Subset of D for f1, f2 being BinOp of D for g1, g2 being BinOp of S st g1 = f1 || S & g2 = f2 || S holds ( ( f1 is_left_distributive_wrt f2 implies g1 is_left_distributive_wrt g2 ) & ( f1 is_right_distributive_wrt f2 implies g1 is_right_distributive_wrt g2 ) ) let S be non empty Subset of D; ::_thesis: for f1, f2 being BinOp of D for g1, g2 being BinOp of S st g1 = f1 || S & g2 = f2 || S holds ( ( f1 is_left_distributive_wrt f2 implies g1 is_left_distributive_wrt g2 ) & ( f1 is_right_distributive_wrt f2 implies g1 is_right_distributive_wrt g2 ) ) let f1, f2 be BinOp of D; ::_thesis: for g1, g2 being BinOp of S st g1 = f1 || S & g2 = f2 || S holds ( ( f1 is_left_distributive_wrt f2 implies g1 is_left_distributive_wrt g2 ) & ( f1 is_right_distributive_wrt f2 implies g1 is_right_distributive_wrt g2 ) ) let g1, g2 be BinOp of S; ::_thesis: ( g1 = f1 || S & g2 = f2 || S implies ( ( f1 is_left_distributive_wrt f2 implies g1 is_left_distributive_wrt g2 ) & ( f1 is_right_distributive_wrt f2 implies g1 is_right_distributive_wrt g2 ) ) ) assume that A1: g1 = f1 || S and A2: g2 = f2 || S ; ::_thesis: ( ( f1 is_left_distributive_wrt f2 implies g1 is_left_distributive_wrt g2 ) & ( f1 is_right_distributive_wrt f2 implies g1 is_right_distributive_wrt g2 ) ) thus ( f1 is_left_distributive_wrt f2 implies g1 is_left_distributive_wrt g2 ) ::_thesis: ( f1 is_right_distributive_wrt f2 implies g1 is_right_distributive_wrt g2 ) proof assume A3: for a, b, c being Element of D holds f1 . (a,(f2 . (b,c))) = f2 . ((f1 . (a,b)),(f1 . (a,c))) ; :: according to BINOP_1:def_18 ::_thesis: g1 is_left_distributive_wrt g2 let a, b, c be Element of S; :: according to BINOP_1:def_18 ::_thesis: g1 . (a,(g2 . (b,c))) = g2 . ((g1 . (a,b)),(g1 . (a,c))) set ab = g1 . (a,b); set ac = g1 . (a,c); set bc = g2 . (b,c); reconsider a9 = a, b9 = b, c9 = c as Element of D ; A4: ( f2 . [b9,c9] = f2 . (b9,c9) & f1 . [a9,b9] = f1 . (a9,b9) ) ; A5: ( f1 . [a9,c9] = f1 . (a9,c9) & f1 . [a,(g2 . (b,c))] = f1 . (a,(g2 . (b,c))) ) ; dom g2 = [:S,S:] by FUNCT_2:def_1; then A6: ( g2 . [b,c] = f2 . [b,c] & g2 . [(g1 . (a,b)),(g1 . (a,c))] = f2 . [(g1 . (a,b)),(g1 . (a,c))] ) by A2, FUNCT_1:47; A7: f2 . [(g1 . (a,b)),(g1 . (a,c))] = f2 . ((g1 . (a,b)),(g1 . (a,c))) ; A8: dom g1 = [:S,S:] by FUNCT_2:def_1; then A9: g1 . [a,(g2 . (b,c))] = f1 . [a,(g2 . (b,c))] by A1, FUNCT_1:47; ( g1 . [a,b] = f1 . [a,b] & g1 . [a,c] = f1 . [a,c] ) by A1, A8, FUNCT_1:47; hence g1 . (a,(g2 . (b,c))) = g2 . ((g1 . (a,b)),(g1 . (a,c))) by A3, A4, A9, A5, A6, A7; ::_thesis: verum end; assume A10: for a, b, c being Element of D holds f1 . ((f2 . (a,b)),c) = f2 . ((f1 . (a,c)),(f1 . (b,c))) ; :: according to BINOP_1:def_19 ::_thesis: g1 is_right_distributive_wrt g2 let a, b, c be Element of S; :: according to BINOP_1:def_19 ::_thesis: g1 . ((g2 . (a,b)),c) = g2 . ((g1 . (a,c)),(g1 . (b,c))) set ab = g2 . (a,b); set ac = g1 . (a,c); set bc = g1 . (b,c); A11: f2 . [(g1 . (a,c)),(g1 . (b,c))] = f2 . ((g1 . (a,c)),(g1 . (b,c))) ; A12: dom g1 = [:S,S:] by FUNCT_2:def_1; then A13: g1 . [(g2 . (a,b)),c] = f1 . [(g2 . (a,b)),c] by A1, FUNCT_1:47; dom g2 = [:S,S:] by FUNCT_2:def_1; then A14: ( g2 . [a,b] = f2 . [a,b] & g2 . [(g1 . (a,c)),(g1 . (b,c))] = f2 . [(g1 . (a,c)),(g1 . (b,c))] ) by A2, FUNCT_1:47; reconsider a9 = a, b9 = b, c9 = c as Element of D ; A15: ( f1 . [b9,c9] = f1 . (b9,c9) & f2 . [a9,b9] = f2 . (a9,b9) ) ; A16: ( f1 . [a9,c9] = f1 . (a9,c9) & f1 . [(g2 . (a,b)),c] = f1 . ((g2 . (a,b)),c) ) ; ( g1 . [b,c] = f1 . [b,c] & g1 . [a,c] = f1 . [a,c] ) by A1, A12, FUNCT_1:47; hence g1 . ((g2 . (a,b)),c) = g2 . ((g1 . (a,c)),(g1 . (b,c))) by A10, A15, A13, A16, A14, A11; ::_thesis: verum end; theorem :: FILTER_2:4 for D being non empty set for S being non empty Subset of D for f1, f2 being BinOp of D for g1, g2 being BinOp of S st g1 = f1 || S & g2 = f2 || S & f1 is_distributive_wrt f2 holds g1 is_distributive_wrt g2 proof let D be non empty set ; ::_thesis: for S being non empty Subset of D for f1, f2 being BinOp of D for g1, g2 being BinOp of S st g1 = f1 || S & g2 = f2 || S & f1 is_distributive_wrt f2 holds g1 is_distributive_wrt g2 let S be non empty Subset of D; ::_thesis: for f1, f2 being BinOp of D for g1, g2 being BinOp of S st g1 = f1 || S & g2 = f2 || S & f1 is_distributive_wrt f2 holds g1 is_distributive_wrt g2 let f1, f2 be BinOp of D; ::_thesis: for g1, g2 being BinOp of S st g1 = f1 || S & g2 = f2 || S & f1 is_distributive_wrt f2 holds g1 is_distributive_wrt g2 let g1, g2 be BinOp of S; ::_thesis: ( g1 = f1 || S & g2 = f2 || S & f1 is_distributive_wrt f2 implies g1 is_distributive_wrt g2 ) assume ( g1 = f1 || S & g2 = f2 || S & f1 is_left_distributive_wrt f2 & f1 is_right_distributive_wrt f2 ) ; :: according to BINOP_1:def_11 ::_thesis: g1 is_distributive_wrt g2 hence ( g1 is_left_distributive_wrt g2 & g1 is_right_distributive_wrt g2 ) by Th3; :: according to BINOP_1:def_11 ::_thesis: verum end; theorem Th5: :: FILTER_2:5 for D being non empty set for S being non empty Subset of D for f1, f2 being BinOp of D for g1, g2 being BinOp of S st g1 = f1 || S & g2 = f2 || S & f1 absorbs f2 holds g1 absorbs g2 proof let D be non empty set ; ::_thesis: for S being non empty Subset of D for f1, f2 being BinOp of D for g1, g2 being BinOp of S st g1 = f1 || S & g2 = f2 || S & f1 absorbs f2 holds g1 absorbs g2 let S be non empty Subset of D; ::_thesis: for f1, f2 being BinOp of D for g1, g2 being BinOp of S st g1 = f1 || S & g2 = f2 || S & f1 absorbs f2 holds g1 absorbs g2 let f1, f2 be BinOp of D; ::_thesis: for g1, g2 being BinOp of S st g1 = f1 || S & g2 = f2 || S & f1 absorbs f2 holds g1 absorbs g2 let g1, g2 be BinOp of S; ::_thesis: ( g1 = f1 || S & g2 = f2 || S & f1 absorbs f2 implies g1 absorbs g2 ) assume that A1: g1 = f1 || S and A2: g2 = f2 || S ; ::_thesis: ( not f1 absorbs f2 or g1 absorbs g2 ) assume A3: for a, b being Element of D holds f1 . (a,(f2 . (a,b))) = a ; :: according to LATTICE2:def_1 ::_thesis: g1 absorbs g2 let a, b be Element of S; :: according to LATTICE2:def_1 ::_thesis: g1 . (a,(g2 . (a,b))) = a A4: dom g2 = [:S,S:] by FUNCT_2:def_1; dom g1 = [:S,S:] by FUNCT_2:def_1; hence g1 . (a,(g2 . (a,b))) = f1 . [a,(g2 . (a,b))] by A1, FUNCT_1:47 .= f1 . [a,(f2 . [a,b])] by A2, A4, FUNCT_1:47 .= f1 . (a,(f2 . (a,b))) .= a by A3 ; ::_thesis: verum end; begin definition let D be non empty set ; let X1, X2 be Subset of D; :: original: = redefine predX1 = X2 means :: FILTER_2:def 1 for x being Element of D holds ( x in X1 iff x in X2 ); compatibility ( X1 = X2 iff for x being Element of D holds ( x in X1 iff x in X2 ) ) by SUBSET_1:3; end; :: deftheorem defines = FILTER_2:def_1_:_ for D being non empty set for X1, X2 being Subset of D holds ( X1 = X2 iff for x being Element of D holds ( x in X1 iff x in X2 ) ); deffunc H1( LattStr ) -> set = the carrier of $1; deffunc H2( LattStr ) -> Element of bool [:[: the carrier of $1, the carrier of $1:], the carrier of $1:] = the L_join of $1; deffunc H3( LattStr ) -> Element of bool [:[: the carrier of $1, the carrier of $1:], the carrier of $1:] = the L_meet of $1; theorem :: FILTER_2:6 for L1, L2 being LattStr st LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) holds L1 .: = L2 .: ; theorem :: FILTER_2:7 for L being Lattice holds (L .:) .: = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) ; theorem :: FILTER_2:8 for L1, L2 being non empty LattStr st LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) holds for a1, b1 being Element of L1 for a2, b2 being Element of L2 st a1 = a2 & b1 = b2 holds ( a1 "\/" b1 = a2 "\/" b2 & a1 "/\" b1 = a2 "/\" b2 & ( a1 [= b1 implies a2 [= b2 ) & ( a2 [= b2 implies a1 [= b1 ) ) proof let L1, L2 be non empty LattStr ; ::_thesis: ( LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) implies for a1, b1 being Element of L1 for a2, b2 being Element of L2 st a1 = a2 & b1 = b2 holds ( a1 "\/" b1 = a2 "\/" b2 & a1 "/\" b1 = a2 "/\" b2 & ( a1 [= b1 implies a2 [= b2 ) & ( a2 [= b2 implies a1 [= b1 ) ) ) assume A1: LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) ; ::_thesis: for a1, b1 being Element of L1 for a2, b2 being Element of L2 st a1 = a2 & b1 = b2 holds ( a1 "\/" b1 = a2 "\/" b2 & a1 "/\" b1 = a2 "/\" b2 & ( a1 [= b1 implies a2 [= b2 ) & ( a2 [= b2 implies a1 [= b1 ) ) let a1, b1 be Element of L1; ::_thesis: for a2, b2 being Element of L2 st a1 = a2 & b1 = b2 holds ( a1 "\/" b1 = a2 "\/" b2 & a1 "/\" b1 = a2 "/\" b2 & ( a1 [= b1 implies a2 [= b2 ) & ( a2 [= b2 implies a1 [= b1 ) ) let a2, b2 be Element of L2; ::_thesis: ( a1 = a2 & b1 = b2 implies ( a1 "\/" b1 = a2 "\/" b2 & a1 "/\" b1 = a2 "/\" b2 & ( a1 [= b1 implies a2 [= b2 ) & ( a2 [= b2 implies a1 [= b1 ) ) ) assume A2: ( a1 = a2 & b1 = b2 ) ; ::_thesis: ( a1 "\/" b1 = a2 "\/" b2 & a1 "/\" b1 = a2 "/\" b2 & ( a1 [= b1 implies a2 [= b2 ) & ( a2 [= b2 implies a1 [= b1 ) ) thus a1 "\/" b1 = a2 "\/" b2 by A1, A2; ::_thesis: ( a1 "/\" b1 = a2 "/\" b2 & ( a1 [= b1 implies a2 [= b2 ) & ( a2 [= b2 implies a1 [= b1 ) ) thus a1 "/\" b1 = a2 "/\" b2 by A1, A2; ::_thesis: ( ( a1 [= b1 implies a2 [= b2 ) & ( a2 [= b2 implies a1 [= b1 ) ) A3: ( a2 "\/" b2 = b2 iff a2 [= b2 ) by LATTICES:def_3; ( a1 [= b1 iff a1 "\/" b1 = b1 ) by LATTICES:def_3; hence ( ( a1 [= b1 implies a2 [= b2 ) & ( a2 [= b2 implies a1 [= b1 ) ) by A1, A2, A3; ::_thesis: verum end; theorem Th9: :: FILTER_2:9 for L1, L2 being 0_Lattice st LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) holds Bottom L1 = Bottom L2 proof let L1, L2 be 0_Lattice; ::_thesis: ( LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) implies Bottom L1 = Bottom L2 ) assume A1: LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) ; ::_thesis: Bottom L1 = Bottom L2 then reconsider c = Bottom L1 as Element of L2 ; now__::_thesis:_for_a_being_Element_of_L2_holds_ (_c_"/\"_a_=_c_&_a_"/\"_c_=_c_) let a be Element of L2; ::_thesis: ( c "/\" a = c & a "/\" c = c ) reconsider b = a as Element of L1 by A1; (Bottom L1) "/\" b = Bottom L1 ; hence c "/\" a = c by A1; ::_thesis: a "/\" c = c hence a "/\" c = c ; ::_thesis: verum end; hence Bottom L1 = Bottom L2 by LATTICES:def_16; ::_thesis: verum end; theorem Th10: :: FILTER_2:10 for L1, L2 being 1_Lattice st LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) holds Top L1 = Top L2 proof let L1, L2 be 1_Lattice; ::_thesis: ( LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) implies Top L1 = Top L2 ) assume A1: LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) ; ::_thesis: Top L1 = Top L2 then reconsider c = Top L1 as Element of L2 ; now__::_thesis:_for_a_being_Element_of_L2_holds_ (_c_"\/"_a_=_c_&_a_"\/"_c_=_c_) let a be Element of L2; ::_thesis: ( c "\/" a = c & a "\/" c = c ) reconsider b = a as Element of L1 by A1; (Top L1) "\/" b = Top L1 ; hence c "\/" a = c by A1; ::_thesis: a "\/" c = c hence a "\/" c = c ; ::_thesis: verum end; hence Top L1 = Top L2 by LATTICES:def_17; ::_thesis: verum end; theorem Th11: :: FILTER_2:11 for L1, L2 being C_Lattice st LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) holds for a1, b1 being Element of L1 for a2, b2 being Element of L2 st a1 = a2 & b1 = b2 & a1 is_a_complement_of b1 holds a2 is_a_complement_of b2 proof let L1, L2 be C_Lattice; ::_thesis: ( LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) implies for a1, b1 being Element of L1 for a2, b2 being Element of L2 st a1 = a2 & b1 = b2 & a1 is_a_complement_of b1 holds a2 is_a_complement_of b2 ) assume A1: LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) ; ::_thesis: for a1, b1 being Element of L1 for a2, b2 being Element of L2 st a1 = a2 & b1 = b2 & a1 is_a_complement_of b1 holds a2 is_a_complement_of b2 let a1, b1 be Element of L1; ::_thesis: for a2, b2 being Element of L2 st a1 = a2 & b1 = b2 & a1 is_a_complement_of b1 holds a2 is_a_complement_of b2 let a2, b2 be Element of L2; ::_thesis: ( a1 = a2 & b1 = b2 & a1 is_a_complement_of b1 implies a2 is_a_complement_of b2 ) assume ( a1 = a2 & b1 = b2 ) ; ::_thesis: ( not a1 is_a_complement_of b1 or a2 is_a_complement_of b2 ) then A2: ( a2 "\/" b2 = a1 "\/" b1 & a2 "/\" b2 = a1 "/\" b1 ) by A1; assume a1 is_a_complement_of b1 ; ::_thesis: a2 is_a_complement_of b2 then ( a1 "\/" b1 = Top L1 & a1 "/\" b1 = Bottom L1 ) by LATTICES:def_18; hence ( a2 "\/" b2 = Top L2 & b2 "\/" a2 = Top L2 & a2 "/\" b2 = Bottom L2 & b2 "/\" a2 = Bottom L2 ) by A1, A2, Th9, Th10; :: according to LATTICES:def_18 ::_thesis: verum end; theorem :: FILTER_2:12 for L1, L2 being B_Lattice st LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) holds for a being Element of L1 for b being Element of L2 st a = b holds a ` = b ` proof let L1, L2 be B_Lattice; ::_thesis: ( LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) implies for a being Element of L1 for b being Element of L2 st a = b holds a ` = b ` ) assume A1: LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) ; ::_thesis: for a being Element of L1 for b being Element of L2 st a = b holds a ` = b ` let a be Element of L1; ::_thesis: for b being Element of L2 st a = b holds a ` = b ` let b be Element of L2; ::_thesis: ( a = b implies a ` = b ` ) assume A2: a = b ; ::_thesis: a ` = b ` reconsider b9 = a ` as Element of L2 by A1; a ` is_a_complement_of a by LATTICES:def_21; then b9 is_a_complement_of b by A1, A2, Th11; hence a ` = b ` by LATTICES:def_21; ::_thesis: verum end; theorem :: FILTER_2:13 for L being Lattice for X being Subset of L st ( for p, q being Element of L holds ( ( p in X & q in X ) iff p "/\" q in X ) ) holds X is ClosedSubset of L proof let L be Lattice; ::_thesis: for X being Subset of L st ( for p, q being Element of L holds ( ( p in X & q in X ) iff p "/\" q in X ) ) holds X is ClosedSubset of L let X be Subset of L; ::_thesis: ( ( for p, q being Element of L holds ( ( p in X & q in X ) iff p "/\" q in X ) ) implies X is ClosedSubset of L ) assume A1: for p, q being Element of L holds ( ( p in X & q in X ) iff p "/\" q in X ) ; ::_thesis: X is ClosedSubset of L for p, q being Element of L st p in X & q in X holds p "\/" q in X proof let p, q be Element of L; ::_thesis: ( p in X & q in X implies p "\/" q in X ) p "/\" (p "\/" q) = p by LATTICES:def_9; hence ( p in X & q in X implies p "\/" q in X ) by A1; ::_thesis: verum end; hence X is ClosedSubset of L by A1, LATTICES:def_24, LATTICES:def_25; ::_thesis: verum end; theorem :: FILTER_2:14 for L being Lattice for X being Subset of L st ( for p, q being Element of L holds ( ( p in X & q in X ) iff p "\/" q in X ) ) holds X is ClosedSubset of L proof let L be Lattice; ::_thesis: for X being Subset of L st ( for p, q being Element of L holds ( ( p in X & q in X ) iff p "\/" q in X ) ) holds X is ClosedSubset of L let X be Subset of L; ::_thesis: ( ( for p, q being Element of L holds ( ( p in X & q in X ) iff p "\/" q in X ) ) implies X is ClosedSubset of L ) assume A1: for p, q being Element of L holds ( ( p in X & q in X ) iff p "\/" q in X ) ; ::_thesis: X is ClosedSubset of L for p, q being Element of L st p in X & q in X holds p "/\" q in X proof let p, q be Element of L; ::_thesis: ( p in X & q in X implies p "/\" q in X ) (p "/\" q) "\/" q = q by LATTICES:def_8; hence ( p in X & q in X implies p "/\" q in X ) by A1; ::_thesis: verum end; hence X is ClosedSubset of L by A1, LATTICES:def_24, LATTICES:def_25; ::_thesis: verum end; definition let L be Lattice; mode Ideal of L is non empty initial join-closed Subset of L; end; Lm1: for L being Lattice for S being non empty Subset of L holds ( S is Ideal of L iff for p, q being Element of L holds ( ( p in S & q in S ) iff p "\/" q in S ) ) proof let L be Lattice; ::_thesis: for S being non empty Subset of L holds ( S is Ideal of L iff for p, q being Element of L holds ( ( p in S & q in S ) iff p "\/" q in S ) ) let S be non empty Subset of L; ::_thesis: ( S is Ideal of L iff for p, q being Element of L holds ( ( p in S & q in S ) iff p "\/" q in S ) ) thus ( S is Ideal of L implies for p, q being Element of L holds ( ( p in S & q in S ) iff p "\/" q in S ) ) ::_thesis: ( ( for p, q being Element of L holds ( ( p in S & q in S ) iff p "\/" q in S ) ) implies S is Ideal of L ) proof assume A1: S is Ideal of L ; ::_thesis: for p, q being Element of L holds ( ( p in S & q in S ) iff p "\/" q in S ) let p, q be Element of L; ::_thesis: ( ( p in S & q in S ) iff p "\/" q in S ) thus ( p in S & q in S implies p "\/" q in S ) by A1, LATTICES:def_25; ::_thesis: ( p "\/" q in S implies ( p in S & q in S ) ) assume A2: p "\/" q in S ; ::_thesis: ( p in S & q in S ) ( p [= p "\/" q & q [= p "\/" q ) by LATTICES:5; hence ( p in S & q in S ) by A1, A2, LATTICES:def_22; ::_thesis: verum end; assume A3: for p, q being Element of L holds ( ( p in S & q in S ) iff p "\/" q in S ) ; ::_thesis: S is Ideal of L S is initial proof let p, q be Element of L; :: according to LATTICES:def_22 ::_thesis: ( not p [= q or not q in S or p in S ) assume that A4: p [= q and A5: q in S ; ::_thesis: p in S p "\/" q = q by A4, LATTICES:def_3; hence p in S by A3, A5; ::_thesis: verum end; hence S is Ideal of L by A3, LATTICES:def_25; ::_thesis: verum end; theorem Th15: :: FILTER_2:15 for L1, L2 being Lattice st LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) holds for x being set st x is Filter of L1 holds x is Filter of L2 proof let L1, L2 be Lattice; ::_thesis: ( LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) implies for x being set st x is Filter of L1 holds x is Filter of L2 ) assume A1: LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) ; ::_thesis: for x being set st x is Filter of L1 holds x is Filter of L2 let x be set ; ::_thesis: ( x is Filter of L1 implies x is Filter of L2 ) assume x is Filter of L1 ; ::_thesis: x is Filter of L2 then reconsider F = x as Filter of L1 ; now__::_thesis:_for_a,_b_being_Element_of_L2_holds_ (_(_a_in_F_&_b_in_F_)_iff_a_"/\"_b_in_F_) let a, b be Element of L2; ::_thesis: ( ( a in F & b in F ) iff a "/\" b in F ) reconsider a9 = a, b9 = b as Element of L1 by A1; a "/\" b = a9 "/\" b9 by A1; hence ( ( a in F & b in F ) iff a "/\" b in F ) by FILTER_0:8; ::_thesis: verum end; hence x is Filter of L2 by A1, FILTER_0:8; ::_thesis: verum end; theorem Th16: :: FILTER_2:16 for L1, L2 being Lattice st LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) holds for x being set st x is Ideal of L1 holds x is Ideal of L2 proof let L1, L2 be Lattice; ::_thesis: ( LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) implies for x being set st x is Ideal of L1 holds x is Ideal of L2 ) assume A1: LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) ; ::_thesis: for x being set st x is Ideal of L1 holds x is Ideal of L2 let x be set ; ::_thesis: ( x is Ideal of L1 implies x is Ideal of L2 ) assume x is Ideal of L1 ; ::_thesis: x is Ideal of L2 then reconsider F = x as Ideal of L1 ; now__::_thesis:_for_a,_b_being_Element_of_L2_holds_ (_(_a_in_F_&_b_in_F_)_iff_a_"\/"_b_in_F_) let a, b be Element of L2; ::_thesis: ( ( a in F & b in F ) iff a "\/" b in F ) reconsider a9 = a, b9 = b as Element of L1 by A1; a "\/" b = a9 "\/" b9 by A1; hence ( ( a in F & b in F ) iff a "\/" b in F ) by Lm1; ::_thesis: verum end; hence x is Ideal of L2 by A1, Lm1; ::_thesis: verum end; definition let L be Lattice; let p be Element of L; funcp .: -> Element of (L .:) equals :: FILTER_2:def 2 p; coherence p is Element of (L .:) ; end; :: deftheorem defines .: FILTER_2:def_2_:_ for L being Lattice for p being Element of L holds p .: = p; definition let L be Lattice; let p be Element of (L .:); func .: p -> Element of L equals :: FILTER_2:def 3 p; coherence p is Element of L ; end; :: deftheorem defines .: FILTER_2:def_3_:_ for L being Lattice for p being Element of (L .:) holds .: p = p; theorem :: FILTER_2:17 for L being Lattice for p being Element of L for p9 being Element of (L .:) holds ( .: (p .:) = p & (.: p9) .: = p9 ) ; theorem :: FILTER_2:18 for L being Lattice for p, q being Element of L for p9, q9 being Element of (L .:) holds ( p "/\" q = (p .:) "\/" (q .:) & p "\/" q = (p .:) "/\" (q .:) & p9 "/\" q9 = (.: p9) "\/" (.: q9) & p9 "\/" q9 = (.: p9) "/\" (.: q9) ) ; theorem :: FILTER_2:19 for L being Lattice for p, q being Element of L for p9, q9 being Element of (L .:) holds ( ( p [= q implies q .: [= p .: ) & ( q .: [= p .: implies p [= q ) & ( p9 [= q9 implies .: q9 [= .: p9 ) & ( .: q9 [= .: p9 implies p9 [= q9 ) ) by LATTICE2:38, LATTICE2:39; definition let L be Lattice; let X be Subset of L; funcX .: -> Subset of (L .:) equals :: FILTER_2:def 4 X; coherence X is Subset of (L .:) ; end; :: deftheorem defines .: FILTER_2:def_4_:_ for L being Lattice for X being Subset of L holds X .: = X; definition let L be Lattice; let X be Subset of (L .:); func .: X -> Subset of L equals :: FILTER_2:def 5 X; coherence X is Subset of L ; end; :: deftheorem defines .: FILTER_2:def_5_:_ for L being Lattice for X being Subset of (L .:) holds .: X = X; registration let L be Lattice; let D be non empty Subset of L; clusterD .: -> non empty ; coherence not D .: is empty ; end; registration let L be Lattice; let D be non empty Subset of (L .:); cluster .: D -> non empty ; coherence not .: D is empty ; end; registration let L be Lattice; let S be meet-closed Subset of L; clusterS .: -> join-closed for Subset of (L .:); coherence for b1 being Subset of (L .:) st b1 = S .: holds b1 is join-closed proof S .: is join-closed proof let p9 be Element of (L .:); :: according to LATTICES:def_25 ::_thesis: for b1 being Element of the carrier of (L .:) holds ( not p9 in S .: or not b1 in S .: or p9 "\/" b1 in S .: ) let q9 be Element of (L .:); ::_thesis: ( not p9 in S .: or not q9 in S .: or p9 "\/" q9 in S .: ) p9 "\/" q9 = (.: p9) "/\" (.: q9) ; hence ( not p9 in S .: or not q9 in S .: or p9 "\/" q9 in S .: ) by LATTICES:def_24; ::_thesis: verum end; hence for b1 being Subset of (L .:) st b1 = S .: holds b1 is join-closed ; ::_thesis: verum end; end; registration let L be Lattice; let S be join-closed Subset of L; clusterS .: -> meet-closed for Subset of (L .:); coherence for b1 being Subset of (L .:) st b1 = S .: holds b1 is meet-closed proof S .: is meet-closed proof let p9 be Element of (L .:); :: according to LATTICES:def_24 ::_thesis: for b1 being Element of the carrier of (L .:) holds ( not p9 in S .: or not b1 in S .: or p9 "/\" b1 in S .: ) let q9 be Element of (L .:); ::_thesis: ( not p9 in S .: or not q9 in S .: or p9 "/\" q9 in S .: ) p9 "/\" q9 = (.: p9) "\/" (.: q9) ; hence ( not p9 in S .: or not q9 in S .: or p9 "/\" q9 in S .: ) by LATTICES:def_25; ::_thesis: verum end; hence for b1 being Subset of (L .:) st b1 = S .: holds b1 is meet-closed ; ::_thesis: verum end; end; registration let L be Lattice; let S be meet-closed Subset of (L .:); cluster .: S -> join-closed for Subset of L; coherence for b1 being Subset of L st b1 = .: S holds b1 is join-closed proof .: S is join-closed proof let p be Element of L; :: according to LATTICES:def_25 ::_thesis: for b1 being Element of the carrier of L holds ( not p in .: S or not b1 in .: S or p "\/" b1 in .: S ) let q be Element of L; ::_thesis: ( not p in .: S or not q in .: S or p "\/" q in .: S ) p "\/" q = (p .:) "/\" (q .:) ; hence ( not p in .: S or not q in .: S or p "\/" q in .: S ) by LATTICES:def_24; ::_thesis: verum end; hence for b1 being Subset of L st b1 = .: S holds b1 is join-closed ; ::_thesis: verum end; end; registration let L be Lattice; let S be join-closed Subset of (L .:); cluster .: S -> meet-closed for Subset of L; coherence for b1 being Subset of L st b1 = .: S holds b1 is meet-closed proof .: S is meet-closed proof let p be Element of L; :: according to LATTICES:def_24 ::_thesis: for b1 being Element of the carrier of L holds ( not p in .: S or not b1 in .: S or p "/\" b1 in .: S ) let q be Element of L; ::_thesis: ( not p in .: S or not q in .: S or p "/\" q in .: S ) p "/\" q = (p .:) "\/" (q .:) ; hence ( not p in .: S or not q in .: S or p "/\" q in .: S ) by LATTICES:def_25; ::_thesis: verum end; hence for b1 being Subset of L st b1 = .: S holds b1 is meet-closed ; ::_thesis: verum end; end; registration let L be Lattice; let F be final Subset of L; clusterF .: -> initial for Subset of (L .:); coherence for b1 being Subset of (L .:) st b1 = F .: holds b1 is initial proof F .: is initial proof let p9 be Element of (L .:); :: according to LATTICES:def_22 ::_thesis: for b1 being Element of the carrier of (L .:) holds ( not p9 [= b1 or not b1 in F .: or p9 in F .: ) let q9 be Element of (L .:); ::_thesis: ( not p9 [= q9 or not q9 in F .: or p9 in F .: ) assume that A1: p9 [= q9 and A2: q9 in F .: ; ::_thesis: p9 in F .: reconsider p = p9 .: , q = q9 .: as Element of L ; q [= p by A1, LATTICE2:39; hence p9 in F .: by A2, LATTICES:def_23; ::_thesis: verum end; hence for b1 being Subset of (L .:) st b1 = F .: holds b1 is initial ; ::_thesis: verum end; end; registration let L be Lattice; let F be initial Subset of L; clusterF .: -> final for Subset of (L .:); coherence for b1 being Subset of (L .:) st b1 = F .: holds b1 is final proof F .: is final proof let p9 be Element of (L .:); :: according to LATTICES:def_23 ::_thesis: for b1 being Element of the carrier of (L .:) holds ( not p9 [= b1 or not p9 in F .: or b1 in F .: ) let q9 be Element of (L .:); ::_thesis: ( not p9 [= q9 or not p9 in F .: or q9 in F .: ) assume that A1: p9 [= q9 and A2: p9 in F .: ; ::_thesis: q9 in F .: reconsider p = p9 .: , q = q9 .: as Element of L ; q [= p by A1, LATTICE2:39; hence q9 in F .: by A2, LATTICES:def_22; ::_thesis: verum end; hence for b1 being Subset of (L .:) st b1 = F .: holds b1 is final ; ::_thesis: verum end; end; registration let L be Lattice; let F be final Subset of (L .:); cluster .: F -> initial for Subset of L; coherence for b1 being Subset of L st b1 = .: F holds b1 is initial proof .: F is initial proof let p be Element of L; :: according to LATTICES:def_22 ::_thesis: for b1 being Element of the carrier of L holds ( not p [= b1 or not b1 in .: F or p in .: F ) let q be Element of L; ::_thesis: ( not p [= q or not q in .: F or p in .: F ) assume that A1: p [= q and A2: q in .: F ; ::_thesis: p in .: F reconsider p9 = p .: , q9 = q .: as Element of (L .:) ; q9 [= p9 by A1, LATTICE2:38; hence p in .: F by A2, LATTICES:def_23; ::_thesis: verum end; hence for b1 being Subset of L st b1 = .: F holds b1 is initial ; ::_thesis: verum end; end; registration let L be Lattice; let F be initial Subset of (L .:); clusterF .: -> final for Subset of L; coherence for b1 being Subset of L st b1 = F .: holds b1 is final proof .: F is final proof let p be Element of L; :: according to LATTICES:def_23 ::_thesis: for b1 being Element of the carrier of L holds ( not p [= b1 or not p in .: F or b1 in .: F ) let q be Element of L; ::_thesis: ( not p [= q or not p in .: F or q in .: F ) assume that A1: p [= q and A2: p in .: F ; ::_thesis: q in .: F reconsider p9 = p .: , q9 = q .: as Element of (L .:) ; q9 [= p9 by A1, LATTICE2:38; hence q in .: F by A2, LATTICES:def_22; ::_thesis: verum end; hence for b1 being Subset of L st b1 = F .: holds b1 is final ; ::_thesis: verum end; end; theorem Th20: :: FILTER_2:20 for L being Lattice for x being set holds ( x is Ideal of L iff x is Filter of (L .:) ) proof let L be Lattice; ::_thesis: for x being set holds ( x is Ideal of L iff x is Filter of (L .:) ) let x be set ; ::_thesis: ( x is Ideal of L iff x is Filter of (L .:) ) thus ( x is Ideal of L implies x is Filter of (L .:) ) ::_thesis: ( x is Filter of (L .:) implies x is Ideal of L ) proof assume x is Ideal of L ; ::_thesis: x is Filter of (L .:) then reconsider I = x as Ideal of L ; reconsider I = I as non empty Subset of (L .:) ; I is Filter of (L .:) proof now__::_thesis:_for_p9,_q9_being_Element_of_(L_.:)_holds_ (_(_p9_in_I_&_q9_in_I_)_iff_p9_"/\"_q9_in_I_) let p9, q9 be Element of (L .:); ::_thesis: ( ( p9 in I & q9 in I ) iff p9 "/\" q9 in I ) p9 "/\" q9 = (.: p9) "\/" (.: q9) ; hence ( ( p9 in I & q9 in I ) iff p9 "/\" q9 in I ) by Lm1; ::_thesis: verum end; hence I is Filter of (L .:) by FILTER_0:8; ::_thesis: verum end; hence x is Filter of (L .:) ; ::_thesis: verum end; assume x is Filter of (L .:) ; ::_thesis: x is Ideal of L then reconsider F = x as Filter of (L .:) ; reconsider F = F as non empty Subset of L ; now__::_thesis:_for_p,_q_being_Element_of_L_holds_ (_(_p_in_F_&_q_in_F_)_iff_p_"\/"_q_in_F_) let p, q be Element of L; ::_thesis: ( ( p in F & q in F ) iff p "\/" q in F ) (p .:) "/\" (q .:) = p "\/" q ; hence ( ( p in F & q in F ) iff p "\/" q in F ) by FILTER_0:8; ::_thesis: verum end; hence x is Ideal of L by Lm1; ::_thesis: verum end; theorem Th21: :: FILTER_2:21 for L being Lattice for D being non empty Subset of L holds ( D is Ideal of L iff ( ( for p, q being Element of L st p in D & q in D holds p "\/" q in D ) & ( for p, q being Element of L st p in D & q [= p holds q in D ) ) ) proof let L be Lattice; ::_thesis: for D being non empty Subset of L holds ( D is Ideal of L iff ( ( for p, q being Element of L st p in D & q in D holds p "\/" q in D ) & ( for p, q being Element of L st p in D & q [= p holds q in D ) ) ) let D be non empty Subset of L; ::_thesis: ( D is Ideal of L iff ( ( for p, q being Element of L st p in D & q in D holds p "\/" q in D ) & ( for p, q being Element of L st p in D & q [= p holds q in D ) ) ) thus ( D is Ideal of L implies ( ( for p, q being Element of L st p in D & q in D holds p "\/" q in D ) & ( for p, q being Element of L st p in D & q [= p holds q in D ) ) ) ::_thesis: ( ( for p, q being Element of L st p in D & q in D holds p "\/" q in D ) & ( for p, q being Element of L st p in D & q [= p holds q in D ) implies D is Ideal of L ) proof assume A1: D is Ideal of L ; ::_thesis: ( ( for p, q being Element of L st p in D & q in D holds p "\/" q in D ) & ( for p, q being Element of L st p in D & q [= p holds q in D ) ) hence for p, q being Element of L st p in D & q in D holds p "\/" q in D by Lm1; ::_thesis: for p, q being Element of L st p in D & q [= p holds q in D let p, q be Element of L; ::_thesis: ( p in D & q [= p implies q in D ) assume ( p in D & q [= p ) ; ::_thesis: q in D then q "\/" p in D by LATTICES:def_3; hence q in D by A1, Lm1; ::_thesis: verum end; assume A2: ( ( for p, q being Element of L st p in D & q in D holds p "\/" q in D ) & ( for p, q being Element of L st p in D & q [= p holds q in D ) ) ; ::_thesis: D is Ideal of L now__::_thesis:_for_p,_q_being_Element_of_L_holds_ (_(_p_in_D_&_q_in_D_)_iff_p_"\/"_q_in_D_) let p, q be Element of L; ::_thesis: ( ( p in D & q in D ) iff p "\/" q in D ) ( p [= p "\/" q & q [= q "\/" p ) by LATTICES:5; hence ( ( p in D & q in D ) iff p "\/" q in D ) by A2; ::_thesis: verum end; hence D is Ideal of L by Lm1; ::_thesis: verum end; theorem Th22: :: FILTER_2:22 for L being Lattice for p, q being Element of L for I being Ideal of L st p in I holds ( p "/\" q in I & q "/\" p in I ) proof let L be Lattice; ::_thesis: for p, q being Element of L for I being Ideal of L st p in I holds ( p "/\" q in I & q "/\" p in I ) let p, q be Element of L; ::_thesis: for I being Ideal of L st p in I holds ( p "/\" q in I & q "/\" p in I ) let I be Ideal of L; ::_thesis: ( p in I implies ( p "/\" q in I & q "/\" p in I ) ) p "/\" q [= p by LATTICES:6; hence ( p in I implies ( p "/\" q in I & q "/\" p in I ) ) by Th21; ::_thesis: verum end; theorem :: FILTER_2:23 for L being Lattice for I being Ideal of L ex p being Element of L st p in I proof let L be Lattice; ::_thesis: for I being Ideal of L ex p being Element of L st p in I let I be Ideal of L; ::_thesis: ex p being Element of L st p in I set i = the Element of I; the Element of I is Element of L ; hence ex p being Element of L st p in I ; ::_thesis: verum end; theorem :: FILTER_2:24 for L being Lattice for I being Ideal of L st L is lower-bounded holds Bottom L in I proof let L be Lattice; ::_thesis: for I being Ideal of L st L is lower-bounded holds Bottom L in I let I be Ideal of L; ::_thesis: ( L is lower-bounded implies Bottom L in I ) assume L is lower-bounded ; ::_thesis: Bottom L in I then ( Top (L .:) = Bottom L & L .: is upper-bounded ) by LATTICE2:48, LATTICE2:61; then Bottom L in I .: by FILTER_0:11; hence Bottom L in I ; ::_thesis: verum end; theorem :: FILTER_2:25 for L being Lattice st L is lower-bounded holds {(Bottom L)} is Ideal of L proof let L be Lattice; ::_thesis: ( L is lower-bounded implies {(Bottom L)} is Ideal of L ) assume L is lower-bounded ; ::_thesis: {(Bottom L)} is Ideal of L then ( Top (L .:) = Bottom L & L .: is upper-bounded ) by LATTICE2:48, LATTICE2:61; then {(Bottom L)} is Filter of (L .:) by FILTER_0:12; hence {(Bottom L)} is Ideal of L by Th20; ::_thesis: verum end; theorem :: FILTER_2:26 for L being Lattice for p being Element of L st {p} is Ideal of L holds L is lower-bounded proof let L be Lattice; ::_thesis: for p being Element of L st {p} is Ideal of L holds L is lower-bounded let p be Element of L; ::_thesis: ( {p} is Ideal of L implies L is lower-bounded ) assume {p} is Ideal of L ; ::_thesis: L is lower-bounded then {p} is Filter of (L .:) by Th20; then L .: is upper-bounded by FILTER_0:13; hence L is lower-bounded by LATTICE2:48; ::_thesis: verum end; begin theorem Th27: :: FILTER_2:27 for L being Lattice holds the carrier of L is Ideal of L proof let L be Lattice; ::_thesis: the carrier of L is Ideal of L H1(L) is Filter of (L .:) by FILTER_0:14; hence the carrier of L is Ideal of L by Th20; ::_thesis: verum end; definition let L be Lattice; func(.L.> -> Ideal of L equals :: FILTER_2:def 6 the carrier of L; coherence the carrier of L is Ideal of L by Th27; end; :: deftheorem defines (. FILTER_2:def_6_:_ for L being Lattice holds (.L.> = the carrier of L; definition let L be Lattice; let p be Element of L; func(.p.> -> Ideal of L equals :: FILTER_2:def 7 { q where q is Element of L : q [= p } ; coherence { q where q is Element of L : q [= p } is Ideal of L proof set X = { q where q is Element of L : q [= p } ; p in { q where q is Element of L : q [= p } ; then reconsider X = { q where q is Element of L : q [= p } as non empty set ; X c= H1(L) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in H1(L) ) assume x in X ; ::_thesis: x in H1(L) then ex q being Element of L st ( x = q & q [= p ) ; hence x in H1(L) ; ::_thesis: verum end; then reconsider X = X as non empty Subset of L ; now__::_thesis:_for_q,_r_being_Element_of_L_holds_ (_(_q_in_X_&_r_in_X_implies_q_"\/"_r_in_X_)_&_(_q_"\/"_r_in_X_implies_(_q_in_X_&_r_in_X_)_)_) let q, r be Element of L; ::_thesis: ( ( q in X & r in X implies q "\/" r in X ) & ( q "\/" r in X implies ( q in X & r in X ) ) ) thus ( q in X & r in X implies q "\/" r in X ) ::_thesis: ( q "\/" r in X implies ( q in X & r in X ) ) proof assume ( q in X & r in X ) ; ::_thesis: q "\/" r in X then ( ex r being Element of L st ( q = r & r [= p ) & ex q being Element of L st ( r = q & q [= p ) ) ; then q "\/" r [= p by FILTER_0:6; hence q "\/" r in X ; ::_thesis: verum end; assume q "\/" r in X ; ::_thesis: ( q in X & r in X ) then A1: ex s being Element of L st ( q "\/" r = s & s [= p ) ; q [= q "\/" r by LATTICES:5; then A2: q [= p by A1, LATTICES:7; r [= r "\/" q by LATTICES:5; then r [= p by A1, LATTICES:7; hence ( q in X & r in X ) by A2; ::_thesis: verum end; hence { q where q is Element of L : q [= p } is Ideal of L by Lm1; ::_thesis: verum end; end; :: deftheorem defines (. FILTER_2:def_7_:_ for L being Lattice for p being Element of L holds (.p.> = { q where q is Element of L : q [= p } ; theorem Th28: :: FILTER_2:28 for L being Lattice for q, p being Element of L holds ( q in (.p.> iff q [= p ) proof let L be Lattice; ::_thesis: for q, p being Element of L holds ( q in (.p.> iff q [= p ) let q, p be Element of L; ::_thesis: ( q in (.p.> iff q [= p ) ( q in (.p.> iff ex r being Element of L st ( q = r & r [= p ) ) ; hence ( q in (.p.> iff q [= p ) ; ::_thesis: verum end; theorem Th29: :: FILTER_2:29 for L being Lattice for p being Element of L holds ( (.p.> = <.(p .:).) & (.(p .:).> = <.p.) ) proof let L be Lattice; ::_thesis: for p being Element of L holds ( (.p.> = <.(p .:).) & (.(p .:).> = <.p.) ) let p be Element of L; ::_thesis: ( (.p.> = <.(p .:).) & (.(p .:).> = <.p.) ) (.p.> = .: <.(p .:).) proof let q be Element of L; :: according to FILTER_2:def_1 ::_thesis: ( q in (.p.> iff q in .: <.(p .:).) ) A1: ( q .: in <.(p .:).) iff p .: [= q .: ) by FILTER_0:15; ( q in (.p.> iff q [= p ) by Th28; hence ( q in (.p.> iff q in .: <.(p .:).) ) by A1, LATTICE2:38, LATTICE2:39; ::_thesis: verum end; hence (.p.> = <.(p .:).) ; ::_thesis: (.(p .:).> = <.p.) .: (.(p .:).> = <.p.) proof let q be Element of L; :: according to FILTER_2:def_1 ::_thesis: ( q in .: (.(p .:).> iff q in <.p.) ) A2: ( q in <.p.) iff p [= q ) by FILTER_0:15; ( q .: in (.(p .:).> iff q .: [= p .: ) by Th28; hence ( q in .: (.(p .:).> iff q in <.p.) ) by A2, LATTICE2:38, LATTICE2:39; ::_thesis: verum end; hence (.(p .:).> = <.p.) ; ::_thesis: verum end; theorem :: FILTER_2:30 for L being Lattice for p, q being Element of L holds ( p in (.p.> & p "/\" q in (.p.> & q "/\" p in (.p.> ) proof let L be Lattice; ::_thesis: for p, q being Element of L holds ( p in (.p.> & p "/\" q in (.p.> & q "/\" p in (.p.> ) let p, q be Element of L; ::_thesis: ( p in (.p.> & p "/\" q in (.p.> & q "/\" p in (.p.> ) p "/\" q [= p by LATTICES:6; hence ( p in (.p.> & p "/\" q in (.p.> & q "/\" p in (.p.> ) ; ::_thesis: verum end; theorem :: FILTER_2:31 for L being Lattice st L is upper-bounded holds (.L.> = (.(Top L).> proof let L be Lattice; ::_thesis: ( L is upper-bounded implies (.L.> = (.(Top L).> ) assume A1: L is upper-bounded ; ::_thesis: (.L.> = (.(Top L).> then L .: is lower-bounded by LATTICE2:49; then A2: <.(L .:).) = <.(Bottom (L .:)).) by FILTER_0:17; Bottom (L .:) = (Top L) .: by A1, LATTICE2:62; hence (.L.> = (.(Top L).> by A2, Th29; ::_thesis: verum end; definition let L be Lattice; let I be Ideal of L; predI is_max-ideal means :: FILTER_2:def 8 ( I <> the carrier of L & ( for J being Ideal of L st I c= J & J <> the carrier of L holds I = J ) ); end; :: deftheorem defines is_max-ideal FILTER_2:def_8_:_ for L being Lattice for I being Ideal of L holds ( I is_max-ideal iff ( I <> the carrier of L & ( for J being Ideal of L st I c= J & J <> the carrier of L holds I = J ) ) ); theorem Th32: :: FILTER_2:32 for L being Lattice for I being Ideal of L holds ( I is_max-ideal iff I .: is being_ultrafilter ) proof let L be Lattice; ::_thesis: for I being Ideal of L holds ( I is_max-ideal iff I .: is being_ultrafilter ) let I be Ideal of L; ::_thesis: ( I is_max-ideal iff I .: is being_ultrafilter ) thus ( I is_max-ideal implies I .: is being_ultrafilter ) ::_thesis: ( I .: is being_ultrafilter implies I is_max-ideal ) proof assume that A1: I <> H1(L) and A2: for J being Ideal of L st I c= J & J <> H1(L) holds I = J ; :: according to FILTER_2:def_8 ::_thesis: I .: is being_ultrafilter thus I .: <> H1(L .: ) by A1; :: according to FILTER_0:def_3 ::_thesis: for b1 being Element of bool the carrier of (L .:) holds ( not I .: c= b1 or b1 = the carrier of (L .:) or I .: = b1 ) let F be Filter of (L .:); ::_thesis: ( not I .: c= F or F = the carrier of (L .:) or I .: = F ) .: F = F ; hence ( not I .: c= F or F = the carrier of (L .:) or I .: = F ) by A2; ::_thesis: verum end; assume that A3: I .: <> H1(L .: ) and A4: for F being Filter of (L .:) st I .: c= F & F <> H1(L .: ) holds I .: = F ; :: according to FILTER_0:def_3 ::_thesis: I is_max-ideal thus I <> H1(L) by A3; :: according to FILTER_2:def_8 ::_thesis: for J being Ideal of L st I c= J & J <> the carrier of L holds I = J let J be Ideal of L; ::_thesis: ( I c= J & J <> the carrier of L implies I = J ) J .: = J ; hence ( I c= J & J <> the carrier of L implies I = J ) by A4; ::_thesis: verum end; theorem :: FILTER_2:33 for L being Lattice st L is upper-bounded holds for I being Ideal of L st I <> the carrier of L holds ex J being Ideal of L st ( I c= J & J is_max-ideal ) proof let L be Lattice; ::_thesis: ( L is upper-bounded implies for I being Ideal of L st I <> the carrier of L holds ex J being Ideal of L st ( I c= J & J is_max-ideal ) ) assume L is upper-bounded ; ::_thesis: for I being Ideal of L st I <> the carrier of L holds ex J being Ideal of L st ( I c= J & J is_max-ideal ) then A1: L .: is lower-bounded by LATTICE2:49; let I be Ideal of L; ::_thesis: ( I <> the carrier of L implies ex J being Ideal of L st ( I c= J & J is_max-ideal ) ) assume I <> H1(L) ; ::_thesis: ex J being Ideal of L st ( I c= J & J is_max-ideal ) then consider F being Filter of (L .:) such that A2: ( I .: c= F & F is being_ultrafilter ) by A1, FILTER_0:18; take .: F ; ::_thesis: ( I c= .: F & .: F is_max-ideal ) (.: F) .: = .: F ; hence ( I c= .: F & .: F is_max-ideal ) by A2, Th32; ::_thesis: verum end; theorem :: FILTER_2:34 for L being Lattice for p being Element of L st ex r being Element of L st p "\/" r <> p holds (.p.> <> the carrier of L proof let L be Lattice; ::_thesis: for p being Element of L st ex r being Element of L st p "\/" r <> p holds (.p.> <> the carrier of L let p be Element of L; ::_thesis: ( ex r being Element of L st p "\/" r <> p implies (.p.> <> the carrier of L ) given r being Element of L such that A1: p "\/" r <> p ; ::_thesis: (.p.> <> the carrier of L p "\/" r = (p .:) "/\" (r .:) ; then <.(p .:).) <> H1(L .: ) by A1, FILTER_0:19; hence (.p.> <> the carrier of L by Th29; ::_thesis: verum end; theorem :: FILTER_2:35 for L being Lattice for p being Element of L st L is upper-bounded & p <> Top L holds ex I being Ideal of L st ( p in I & I is_max-ideal ) proof let L be Lattice; ::_thesis: for p being Element of L st L is upper-bounded & p <> Top L holds ex I being Ideal of L st ( p in I & I is_max-ideal ) let p be Element of L; ::_thesis: ( L is upper-bounded & p <> Top L implies ex I being Ideal of L st ( p in I & I is_max-ideal ) ) assume L is upper-bounded ; ::_thesis: ( not p <> Top L or ex I being Ideal of L st ( p in I & I is_max-ideal ) ) then A1: ( L .: is lower-bounded & Bottom (L .:) = Top L ) by LATTICE2:49, LATTICE2:62; assume p <> Top L ; ::_thesis: ex I being Ideal of L st ( p in I & I is_max-ideal ) then consider F being Filter of (L .:) such that A2: ( p .: in F & F is being_ultrafilter ) by A1, FILTER_0:20; take .: F ; ::_thesis: ( p in .: F & .: F is_max-ideal ) (.: F) .: = .: F ; hence ( p in .: F & .: F is_max-ideal ) by A2, Th32; ::_thesis: verum end; definition let L be Lattice; let D be non empty Subset of L; func(.D.> -> Ideal of L means :Def9: :: FILTER_2:def 9 ( D c= it & ( for I being Ideal of L st D c= I holds it c= I ) ); existence ex b1 being Ideal of L st ( D c= b1 & ( for I being Ideal of L st D c= I holds b1 c= I ) ) proof take I = .: <.(D .:).); ::_thesis: ( D c= I & ( for I being Ideal of L st D c= I holds I c= I ) ) thus D c= I by FILTER_0:def_4; ::_thesis: for I being Ideal of L st D c= I holds I c= I let J be Ideal of L; ::_thesis: ( D c= J implies I c= J ) J .: = J ; hence ( D c= J implies I c= J ) by FILTER_0:def_4; ::_thesis: verum end; uniqueness for b1, b2 being Ideal of L st D c= b1 & ( for I being Ideal of L st D c= I holds b1 c= I ) & D c= b2 & ( for I being Ideal of L st D c= I holds b2 c= I ) holds b1 = b2 proof let I1, I2 be Ideal of L; ::_thesis: ( D c= I1 & ( for I being Ideal of L st D c= I holds I1 c= I ) & D c= I2 & ( for I being Ideal of L st D c= I holds I2 c= I ) implies I1 = I2 ) assume ( D c= I1 & ( for I being Ideal of L st D c= I holds I1 c= I ) & D c= I2 & ( for I being Ideal of L st D c= I holds I2 c= I ) ) ; ::_thesis: I1 = I2 then ( I1 c= I2 & I2 c= I1 ) ; hence I1 = I2 by XBOOLE_0:def_10; ::_thesis: verum end; end; :: deftheorem Def9 defines (. FILTER_2:def_9_:_ for L being Lattice for D being non empty Subset of L for b3 being Ideal of L holds ( b3 = (.D.> iff ( D c= b3 & ( for I being Ideal of L st D c= I holds b3 c= I ) ) ); Lm2: for L1, L2 being Lattice for D1 being non empty Subset of L1 for D2 being non empty Subset of L2 st LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) & D1 = D2 holds ( <.D1.) = <.D2.) & (.D1.> = (.D2.> ) proof let L1, L2 be Lattice; ::_thesis: for D1 being non empty Subset of L1 for D2 being non empty Subset of L2 st LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) & D1 = D2 holds ( <.D1.) = <.D2.) & (.D1.> = (.D2.> ) let D1 be non empty Subset of L1; ::_thesis: for D2 being non empty Subset of L2 st LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) & D1 = D2 holds ( <.D1.) = <.D2.) & (.D1.> = (.D2.> ) let D2 be non empty Subset of L2; ::_thesis: ( LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) & D1 = D2 implies ( <.D1.) = <.D2.) & (.D1.> = (.D2.> ) ) assume that A1: LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) and A2: D1 = D2 ; ::_thesis: ( <.D1.) = <.D2.) & (.D1.> = (.D2.> ) A3: ( D1 c= <.D1.) & D2 c= <.D2.) ) by FILTER_0:def_4; ( <.D1.) is Filter of L2 & <.D2.) is Filter of L1 ) by A1, Th15; hence ( <.D1.) c= <.D2.) & <.D2.) c= <.D1.) ) by A2, A3, FILTER_0:def_4; :: according to XBOOLE_0:def_10 ::_thesis: (.D1.> = (.D2.> A4: ( D1 c= (.D1.> & D2 c= (.D2.> ) by Def9; ( (.D1.> is Ideal of L2 & (.D2.> is Ideal of L1 ) by A1, Th16; hence ( (.D1.> c= (.D2.> & (.D2.> c= (.D1.> ) by A2, A4, Def9; :: according to XBOOLE_0:def_10 ::_thesis: verum end; theorem Th36: :: FILTER_2:36 for L being Lattice for D being non empty Subset of L for D9 being non empty Subset of (L .:) holds ( <.(D .:).) = (.D.> & <.D.) = (.(D .:).> & <.(.: D9).) = (.D9.> & <.D9.) = (.(.: D9).> ) proof let L be Lattice; ::_thesis: for D being non empty Subset of L for D9 being non empty Subset of (L .:) holds ( <.(D .:).) = (.D.> & <.D.) = (.(D .:).> & <.(.: D9).) = (.D9.> & <.D9.) = (.(.: D9).> ) let D be non empty Subset of L; ::_thesis: for D9 being non empty Subset of (L .:) holds ( <.(D .:).) = (.D.> & <.D.) = (.(D .:).> & <.(.: D9).) = (.D9.> & <.D9.) = (.(.: D9).> ) let D9 be non empty Subset of (L .:); ::_thesis: ( <.(D .:).) = (.D.> & <.D.) = (.(D .:).> & <.(.: D9).) = (.D9.> & <.D9.) = (.(.: D9).> ) A1: for L being Lattice for D being non empty Subset of L holds <.(D .:).) = (.D.> proof let L be Lattice; ::_thesis: for D being non empty Subset of L holds <.(D .:).) = (.D.> let D be non empty Subset of L; ::_thesis: <.(D .:).) = (.D.> (.D.> .: = (.D.> ; then A2: ( D c= (.D.> implies <.(D .:).) c= (.D.> ) by FILTER_0:def_4; .: <.(D .:).) = <.(D .:).) ; then ( D c= <.(D .:).) implies (.D.> c= <.(D .:).) ) by Def9; hence <.(D .:).) = (.D.> by A2, Def9, FILTER_0:def_4, XBOOLE_0:def_10; ::_thesis: verum end; ( <.((D .:) .:).) = <.D.) & <.(((.: D9) .:) .:).) = <.(.: D9).) ) by Lm2; hence ( <.(D .:).) = (.D.> & <.D.) = (.(D .:).> & <.(.: D9).) = (.D9.> & <.D9.) = (.(.: D9).> ) by A1; ::_thesis: verum end; theorem Th37: :: FILTER_2:37 for L being Lattice for I being Ideal of L holds (.I.> = I proof let L be Lattice; ::_thesis: for I being Ideal of L holds (.I.> = I let I be Ideal of L; ::_thesis: (.I.> = I ( (.I.> c= I & I c= (.I.> ) by Def9; hence (.I.> = I by XBOOLE_0:def_10; ::_thesis: verum end; theorem :: FILTER_2:38 for L being Lattice for D, D1, D2 being non empty Subset of L holds ( ( D1 c= D2 implies (.D1.> c= (.D2.> ) & (.(.D.>.> c= (.D.> ) proof let L be Lattice; ::_thesis: for D, D1, D2 being non empty Subset of L holds ( ( D1 c= D2 implies (.D1.> c= (.D2.> ) & (.(.D.>.> c= (.D.> ) let D, D1, D2 be non empty Subset of L; ::_thesis: ( ( D1 c= D2 implies (.D1.> c= (.D2.> ) & (.(.D.>.> c= (.D.> ) D2 c= (.D2.> by Def9; then ( D1 c= D2 implies D1 c= (.D2.> ) by XBOOLE_1:1; hence ( ( D1 c= D2 implies (.D1.> c= (.D2.> ) & (.(.D.>.> c= (.D.> ) by Def9; ::_thesis: verum end; theorem :: FILTER_2:39 for L being Lattice for p being Element of L for D being non empty Subset of L st p in D holds (.p.> c= (.D.> proof let L be Lattice; ::_thesis: for p being Element of L for D being non empty Subset of L st p in D holds (.p.> c= (.D.> let p be Element of L; ::_thesis: for D being non empty Subset of L st p in D holds (.p.> c= (.D.> let D be non empty Subset of L; ::_thesis: ( p in D implies (.p.> c= (.D.> ) ( <.(p .:).) = (.p.> & <.(D .:).) = (.D.> ) by Th29, Th36; hence ( p in D implies (.p.> c= (.D.> ) by FILTER_0:23; ::_thesis: verum end; theorem :: FILTER_2:40 for L being Lattice for p being Element of L for D being non empty Subset of L st D = {p} holds (.D.> = (.p.> proof let L be Lattice; ::_thesis: for p being Element of L for D being non empty Subset of L st D = {p} holds (.D.> = (.p.> let p be Element of L; ::_thesis: for D being non empty Subset of L st D = {p} holds (.D.> = (.p.> let D be non empty Subset of L; ::_thesis: ( D = {p} implies (.D.> = (.p.> ) ( <.(p .:).) = (.p.> & <.(D .:).) = (.D.> ) by Th29, Th36; hence ( D = {p} implies (.D.> = (.p.> ) by FILTER_0:24; ::_thesis: verum end; theorem Th41: :: FILTER_2:41 for L being Lattice for D being non empty Subset of L st L is upper-bounded & Top L in D holds ( (.D.> = (.L.> & (.D.> = the carrier of L ) proof let L be Lattice; ::_thesis: for D being non empty Subset of L st L is upper-bounded & Top L in D holds ( (.D.> = (.L.> & (.D.> = the carrier of L ) let D be non empty Subset of L; ::_thesis: ( L is upper-bounded & Top L in D implies ( (.D.> = (.L.> & (.D.> = the carrier of L ) ) assume L is upper-bounded ; ::_thesis: ( not Top L in D or ( (.D.> = (.L.> & (.D.> = the carrier of L ) ) then A1: ( L .: is lower-bounded & Bottom (L .:) = Top L ) by LATTICE2:49, LATTICE2:62; assume Top L in D ; ::_thesis: ( (.D.> = (.L.> & (.D.> = the carrier of L ) then <.(D .:).) = <.(L .:).) by A1, FILTER_0:25; hence ( (.D.> = (.L.> & (.D.> = the carrier of L ) by Th36; ::_thesis: verum end; theorem :: FILTER_2:42 for L being Lattice for I being Ideal of L st L is upper-bounded & Top L in I holds ( I = (.L.> & I = the carrier of L ) proof let L be Lattice; ::_thesis: for I being Ideal of L st L is upper-bounded & Top L in I holds ( I = (.L.> & I = the carrier of L ) let I be Ideal of L; ::_thesis: ( L is upper-bounded & Top L in I implies ( I = (.L.> & I = the carrier of L ) ) (.I.> = I by Th37; hence ( L is upper-bounded & Top L in I implies ( I = (.L.> & I = the carrier of L ) ) by Th41; ::_thesis: verum end; definition let L be Lattice; let I be Ideal of L; attrI is prime means :: FILTER_2:def 10 for p, q being Element of L holds ( p "/\" q in I iff ( p in I or q in I ) ); end; :: deftheorem defines prime FILTER_2:def_10_:_ for L being Lattice for I being Ideal of L holds ( I is prime iff for p, q being Element of L holds ( p "/\" q in I iff ( p in I or q in I ) ) ); theorem Th43: :: FILTER_2:43 for L being Lattice for I being Ideal of L holds ( I is prime iff I .: is prime ) proof let L be Lattice; ::_thesis: for I being Ideal of L holds ( I is prime iff I .: is prime ) let I be Ideal of L; ::_thesis: ( I is prime iff I .: is prime ) thus ( I is prime implies I .: is prime ) ::_thesis: ( I .: is prime implies I is prime ) proof assume A1: for p, q being Element of L holds ( p "/\" q in I iff ( p in I or q in I ) ) ; :: according to FILTER_2:def_10 ::_thesis: I .: is prime let p9 be Element of (L .:); :: according to FILTER_0:def_5 ::_thesis: for b1 being Element of the carrier of (L .:) holds ( ( not p9 "\/" b1 in I .: or p9 in I .: or b1 in I .: ) & ( ( not p9 in I .: & not b1 in I .: ) or p9 "\/" b1 in I .: ) ) let q9 be Element of (L .:); ::_thesis: ( ( not p9 "\/" q9 in I .: or p9 in I .: or q9 in I .: ) & ( ( not p9 in I .: & not q9 in I .: ) or p9 "\/" q9 in I .: ) ) p9 "\/" q9 = (.: p9) "/\" (.: q9) ; hence ( ( not p9 "\/" q9 in I .: or p9 in I .: or q9 in I .: ) & ( ( not p9 in I .: & not q9 in I .: ) or p9 "\/" q9 in I .: ) ) by A1; ::_thesis: verum end; assume A2: for p9, q9 being Element of (L .:) holds ( p9 "\/" q9 in I .: iff ( p9 in I .: or q9 in I .: ) ) ; :: according to FILTER_0:def_5 ::_thesis: I is prime let p be Element of L; :: according to FILTER_2:def_10 ::_thesis: for q being Element of L holds ( p "/\" q in I iff ( p in I or q in I ) ) let q be Element of L; ::_thesis: ( p "/\" q in I iff ( p in I or q in I ) ) (p .:) "\/" (q .:) = p "/\" q ; hence ( p "/\" q in I iff ( p in I or q in I ) ) by A2; ::_thesis: verum end; definition let L be Lattice; let D1, D2 be non empty Subset of L; funcD1 "\/" D2 -> Subset of L equals :: FILTER_2:def 11 { (p "\/" q) where p, q is Element of L : ( p in D1 & q in D2 ) } ; coherence { (p "\/" q) where p, q is Element of L : ( p in D1 & q in D2 ) } is Subset of L proof set X = { (p "\/" q) where p, q is Element of L : ( p in D1 & q in D2 ) } ; { (p "\/" q) where p, q is Element of L : ( p in D1 & q in D2 ) } c= H1(L) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (p "\/" q) where p, q is Element of L : ( p in D1 & q in D2 ) } or x in H1(L) ) assume x in { (p "\/" q) where p, q is Element of L : ( p in D1 & q in D2 ) } ; ::_thesis: x in H1(L) then ex p, q being Element of L st ( x = p "\/" q & p in D1 & q in D2 ) ; hence x in H1(L) ; ::_thesis: verum end; hence { (p "\/" q) where p, q is Element of L : ( p in D1 & q in D2 ) } is Subset of L ; ::_thesis: verum end; end; :: deftheorem defines "\/" FILTER_2:def_11_:_ for L being Lattice for D1, D2 being non empty Subset of L holds D1 "\/" D2 = { (p "\/" q) where p, q is Element of L : ( p in D1 & q in D2 ) } ; registration let L be Lattice; let D1, D2 be non empty Subset of L; clusterD1 "\/" D2 -> non empty ; coherence not D1 "\/" D2 is empty proof set X = { (p "\/" q) where p, q is Element of L : ( p in D1 & q in D2 ) } ; set p1 = the Element of D1; set p2 = the Element of D2; the Element of D1 "\/" the Element of D2 in { (p "\/" q) where p, q is Element of L : ( p in D1 & q in D2 ) } ; then reconsider X = { (p "\/" q) where p, q is Element of L : ( p in D1 & q in D2 ) } as non empty set ; X = D1 "\/" D2 ; hence not D1 "\/" D2 is empty ; ::_thesis: verum end; end; Lm3: for L1, L2 being Lattice for D1, E1 being non empty Subset of L1 for D2, E2 being non empty Subset of L2 st LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) & D1 = D2 & E1 = E2 holds D1 "/\" E1 = D2 "/\" E2 proof let L1, L2 be Lattice; ::_thesis: for D1, E1 being non empty Subset of L1 for D2, E2 being non empty Subset of L2 st LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) & D1 = D2 & E1 = E2 holds D1 "/\" E1 = D2 "/\" E2 let D1, E1 be non empty Subset of L1; ::_thesis: for D2, E2 being non empty Subset of L2 st LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) & D1 = D2 & E1 = E2 holds D1 "/\" E1 = D2 "/\" E2 let D2, E2 be non empty Subset of L2; ::_thesis: ( LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) & D1 = D2 & E1 = E2 implies D1 "/\" E1 = D2 "/\" E2 ) assume that A1: LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) and A2: ( D1 = D2 & E1 = E2 ) ; ::_thesis: D1 "/\" E1 = D2 "/\" E2 thus D1 "/\" E1 c= D2 "/\" E2 :: according to XBOOLE_0:def_10 ::_thesis: D2 "/\" E2 c= D1 "/\" E1 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D1 "/\" E1 or x in D2 "/\" E2 ) assume x in D1 "/\" E1 ; ::_thesis: x in D2 "/\" E2 then consider a, b being Element of L1 such that A3: x = a "/\" b and A4: ( a in D1 & b in E1 ) ; reconsider a9 = a, b9 = b as Element of L2 by A1; x = a9 "/\" b9 by A1, A3; hence x in D2 "/\" E2 by A2, A4; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D2 "/\" E2 or x in D1 "/\" E1 ) assume x in D2 "/\" E2 ; ::_thesis: x in D1 "/\" E1 then consider a, b being Element of L2 such that A5: x = a "/\" b and A6: ( a in D2 & b in E2 ) ; reconsider a9 = a, b9 = b as Element of L1 by A1; x = a9 "/\" b9 by A1, A5; hence x in D1 "/\" E1 by A2, A6; ::_thesis: verum end; theorem Th44: :: FILTER_2:44 for L being Lattice for D1, D2 being non empty Subset of L for D19, D29 being non empty Subset of (L .:) holds ( D1 "\/" D2 = (D1 .:) "/\" (D2 .:) & (D1 .:) "\/" (D2 .:) = D1 "/\" D2 & D19 "\/" D29 = (.: D19) "/\" (.: D29) & (.: D19) "\/" (.: D29) = D19 "/\" D29 ) proof let L be Lattice; ::_thesis: for D1, D2 being non empty Subset of L for D19, D29 being non empty Subset of (L .:) holds ( D1 "\/" D2 = (D1 .:) "/\" (D2 .:) & (D1 .:) "\/" (D2 .:) = D1 "/\" D2 & D19 "\/" D29 = (.: D19) "/\" (.: D29) & (.: D19) "\/" (.: D29) = D19 "/\" D29 ) let D1, D2 be non empty Subset of L; ::_thesis: for D19, D29 being non empty Subset of (L .:) holds ( D1 "\/" D2 = (D1 .:) "/\" (D2 .:) & (D1 .:) "\/" (D2 .:) = D1 "/\" D2 & D19 "\/" D29 = (.: D19) "/\" (.: D29) & (.: D19) "\/" (.: D29) = D19 "/\" D29 ) let D19, D29 be non empty Subset of (L .:); ::_thesis: ( D1 "\/" D2 = (D1 .:) "/\" (D2 .:) & (D1 .:) "\/" (D2 .:) = D1 "/\" D2 & D19 "\/" D29 = (.: D19) "/\" (.: D29) & (.: D19) "\/" (.: D29) = D19 "/\" D29 ) A1: for L being Lattice for D1, D2 being non empty Subset of L holds D1 "\/" D2 = (D1 .:) "/\" (D2 .:) proof let L be Lattice; ::_thesis: for D1, D2 being non empty Subset of L holds D1 "\/" D2 = (D1 .:) "/\" (D2 .:) let D1, D2 be non empty Subset of L; ::_thesis: D1 "\/" D2 = (D1 .:) "/\" (D2 .:) thus D1 "\/" D2 c= (D1 .:) "/\" (D2 .:) :: according to XBOOLE_0:def_10 ::_thesis: (D1 .:) "/\" (D2 .:) c= D1 "\/" D2 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D1 "\/" D2 or x in (D1 .:) "/\" (D2 .:) ) assume x in D1 "\/" D2 ; ::_thesis: x in (D1 .:) "/\" (D2 .:) then consider p, q being Element of L such that A2: ( x = p "\/" q & p in D1 & q in D2 ) ; p "\/" q = (p .:) "/\" (q .:) ; hence x in (D1 .:) "/\" (D2 .:) by A2; ::_thesis: verum end; thus (D1 .:) "/\" (D2 .:) c= D1 "\/" D2 ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (D1 .:) "/\" (D2 .:) or x in D1 "\/" D2 ) assume x in (D1 .:) "/\" (D2 .:) ; ::_thesis: x in D1 "\/" D2 then consider p9, q9 being Element of (L .:) such that A3: ( x = p9 "/\" q9 & p9 in D1 & q9 in D2 ) ; (.: p9) "\/" (.: q9) = p9 "/\" q9 ; hence x in D1 "\/" D2 by A3; ::_thesis: verum end; end; A4: ( (.: D19) .: = .: D19 & (.: D29) .: = .: D29 ) ; ( ((D1 .:) .:) "/\" ((D2 .:) .:) = D1 "/\" D2 & (D19 .:) "/\" (D29 .:) = (.: D19) "/\" (.: D29) ) by Lm3; hence ( D1 "\/" D2 = (D1 .:) "/\" (D2 .:) & (D1 .:) "\/" (D2 .:) = D1 "/\" D2 & D19 "\/" D29 = (.: D19) "/\" (.: D29) & (.: D19) "\/" (.: D29) = D19 "/\" D29 ) by A1, A4; ::_thesis: verum end; theorem :: FILTER_2:45 for L being Lattice for p, q being Element of L for D1, D2 being non empty Subset of L st p in D1 & q in D2 holds ( p "\/" q in D1 "\/" D2 & q "\/" p in D1 "\/" D2 ) ; theorem :: FILTER_2:46 for L being Lattice for x being set for D1, D2 being non empty Subset of L st x in D1 "\/" D2 holds ex p, q being Element of L st ( x = p "\/" q & p in D1 & q in D2 ) ; theorem :: FILTER_2:47 for L being Lattice for D1, D2 being non empty Subset of L holds D1 "\/" D2 = D2 "\/" D1 proof let L be Lattice; ::_thesis: for D1, D2 being non empty Subset of L holds D1 "\/" D2 = D2 "\/" D1 let D1, D2 be non empty Subset of L; ::_thesis: D1 "\/" D2 = D2 "\/" D1 let r be Element of L; :: according to FILTER_2:def_1 ::_thesis: ( r in D1 "\/" D2 iff r in D2 "\/" D1 ) thus ( r in D1 "\/" D2 implies r in D2 "\/" D1 ) ::_thesis: ( r in D2 "\/" D1 implies r in D1 "\/" D2 ) proof assume r in D1 "\/" D2 ; ::_thesis: r in D2 "\/" D1 then ex p, q being Element of L st ( r = p "\/" q & p in D1 & q in D2 ) ; hence r in D2 "\/" D1 ; ::_thesis: verum end; assume r in D2 "\/" D1 ; ::_thesis: r in D1 "\/" D2 then ex p, q being Element of L st ( r = p "\/" q & p in D2 & q in D1 ) ; hence r in D1 "\/" D2 ; ::_thesis: verum end; registration let L be D_Lattice; let I1, I2 be Ideal of L; clusterI1 "\/" I2 -> initial join-closed ; coherence ( I1 "\/" I2 is initial & I1 "\/" I2 is join-closed ) proof reconsider K = L .: as D_Lattice by LATTICE2:50; reconsider J1 = I1 .: , J2 = I2 .: as Filter of K ; ( I1 "\/" I2 = (I1 .:) "/\" (I2 .:) & J1 "/\" J2 = (J1 "/\" J2) .: ) by Th44; hence ( I1 "\/" I2 is initial & I1 "\/" I2 is join-closed ) by Th16; ::_thesis: verum end; end; theorem :: FILTER_2:48 for L being Lattice for D1, D2 being non empty Subset of L holds ( (.(D1 \/ D2).> = (.((.D1.> \/ D2).> & (.(D1 \/ D2).> = (.(D1 \/ (.D2.>).> ) proof let L be Lattice; ::_thesis: for D1, D2 being non empty Subset of L holds ( (.(D1 \/ D2).> = (.((.D1.> \/ D2).> & (.(D1 \/ D2).> = (.(D1 \/ (.D2.>).> ) let D1, D2 be non empty Subset of L; ::_thesis: ( (.(D1 \/ D2).> = (.((.D1.> \/ D2).> & (.(D1 \/ D2).> = (.(D1 \/ (.D2.>).> ) A1: ( (.(D1 \/ (.D2.>).> = <.((D1 \/ (.D2.>) .:).) & (.D2.> = <.(D2 .:).) ) by Th36; A2: (.(D1 \/ D2).> = <.((D1 \/ D2) .:).) by Th36; ( (.((.D1.> \/ D2).> = <.(((.D1.> \/ D2) .:).) & (.D1.> = <.(D1 .:).) ) by Th36; hence ( (.(D1 \/ D2).> = (.((.D1.> \/ D2).> & (.(D1 \/ D2).> = (.(D1 \/ (.D2.>).> ) by A1, A2, FILTER_0:34; ::_thesis: verum end; theorem :: FILTER_2:49 for L being Lattice for I, J being Ideal of L holds (.(I \/ J).> = { r where r is Element of L : ex p, q being Element of L st ( r [= p "\/" q & p in I & q in J ) } proof let L be Lattice; ::_thesis: for I, J being Ideal of L holds (.(I \/ J).> = { r where r is Element of L : ex p, q being Element of L st ( r [= p "\/" q & p in I & q in J ) } let I, J be Ideal of L; ::_thesis: (.(I \/ J).> = { r where r is Element of L : ex p, q being Element of L st ( r [= p "\/" q & p in I & q in J ) } A1: J .: = J ; ( (.(I \/ J).> = <.((I \/ J) .:).) & I .: = I ) by Th36; then A2: (.(I \/ J).> = { r9 where r9 is Element of (L .:) : ex p9, q9 being Element of (L .:) st ( p9 "/\" q9 [= r9 & p9 in I & q9 in J ) } by A1, FILTER_0:35; thus (.(I \/ J).> c= { r where r is Element of L : ex p, q being Element of L st ( r [= p "\/" q & p in I & q in J ) } :: according to XBOOLE_0:def_10 ::_thesis: { r where r is Element of L : ex p, q being Element of L st ( r [= p "\/" q & p in I & q in J ) } c= (.(I \/ J).> proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (.(I \/ J).> or x in { r where r is Element of L : ex p, q being Element of L st ( r [= p "\/" q & p in I & q in J ) } ) assume x in (.(I \/ J).> ; ::_thesis: x in { r where r is Element of L : ex p, q being Element of L st ( r [= p "\/" q & p in I & q in J ) } then consider r9 being Element of (L .:) such that A3: x = r9 and A4: ex p9, q9 being Element of (L .:) st ( p9 "/\" q9 [= r9 & p9 in I & q9 in J ) by A2; consider p9, q9 being Element of (L .:) such that A5: p9 "/\" q9 [= r9 and A6: ( p9 in I & q9 in J ) by A4; A7: p9 "/\" q9 = (.: p9) "\/" (.: q9) ; .: r9 [= .: (p9 "/\" q9) by A5, LATTICE2:39; hence x in { r where r is Element of L : ex p, q being Element of L st ( r [= p "\/" q & p in I & q in J ) } by A3, A6, A7; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { r where r is Element of L : ex p, q being Element of L st ( r [= p "\/" q & p in I & q in J ) } or x in (.(I \/ J).> ) assume x in { r where r is Element of L : ex p, q being Element of L st ( r [= p "\/" q & p in I & q in J ) } ; ::_thesis: x in (.(I \/ J).> then consider r being Element of L such that A8: x = r and A9: ex p, q being Element of L st ( r [= p "\/" q & p in I & q in J ) ; consider p, q being Element of L such that A10: r [= p "\/" q and A11: ( p in I & q in J ) by A9; A12: p "\/" q = (p .:) "/\" (q .:) ; (p "\/" q) .: [= r .: by A10, LATTICE2:38; hence x in (.(I \/ J).> by A2, A8, A11, A12; ::_thesis: verum end; theorem :: FILTER_2:50 for L being Lattice for I, J being Ideal of L holds ( I c= I "\/" J & J c= I "\/" J ) proof let L be Lattice; ::_thesis: for I, J being Ideal of L holds ( I c= I "\/" J & J c= I "\/" J ) let I, J be Ideal of L; ::_thesis: ( I c= I "\/" J & J c= I "\/" J ) I "\/" J = (I .:) "/\" (J .:) by Th44; hence ( I c= I "\/" J & J c= I "\/" J ) by FILTER_0:36; ::_thesis: verum end; theorem :: FILTER_2:51 for L being Lattice for I, J being Ideal of L holds (.(I \/ J).> = (.(I "\/" J).> proof let L be Lattice; ::_thesis: for I, J being Ideal of L holds (.(I \/ J).> = (.(I "\/" J).> let I, J be Ideal of L; ::_thesis: (.(I \/ J).> = (.(I "\/" J).> A1: (.(I "\/" J).> = <.((I "\/" J) .:).) by Th36; ( (.(I \/ J).> = <.((I \/ J) .:).) & (I .:) "/\" (J .:) = I "\/" J ) by Th36, Th44; hence (.(I \/ J).> = (.(I "\/" J).> by A1, FILTER_0:37; ::_thesis: verum end; theorem Th52: :: FILTER_2:52 for L being Lattice holds ( L is C_Lattice iff L .: is C_Lattice ) proof let L be Lattice; ::_thesis: ( L is C_Lattice iff L .: is C_Lattice ) A1: ( L is upper-bounded iff L .: is lower-bounded ) by LATTICE2:49; A2: ( L is lower-bounded iff L .: is upper-bounded ) by LATTICE2:48; thus ( L is C_Lattice implies L .: is C_Lattice ) ::_thesis: ( L .: is C_Lattice implies L is C_Lattice ) proof assume A3: L is C_Lattice ; ::_thesis: L .: is C_Lattice now__::_thesis:_for_p9_being_Element_of_(L_.:)_ex_r_being_Element_of_(L_.:)_st_r_is_a_complement_of_p9 let p9 be Element of (L .:); ::_thesis: ex r being Element of (L .:) st r is_a_complement_of p9 consider q being Element of L such that A4: q is_a_complement_of .: p9 by A3, LATTICES:def_19; take r = q .: ; ::_thesis: r is_a_complement_of p9 q "\/" (.: p9) = Top L by A4, LATTICES:def_18; then A5: (q .:) "/\" p9 = Top L ; q "/\" (.: p9) = Bottom L by A4, LATTICES:def_18; then A6: (q .:) "\/" p9 = Bottom L ; ( Top (L .:) = Bottom L & Bottom (L .:) = Top L ) by A3, LATTICE2:61, LATTICE2:62; hence r is_a_complement_of p9 by A5, A6, LATTICES:def_18; ::_thesis: verum end; hence L .: is C_Lattice by A2, A1, A3, LATTICES:def_19; ::_thesis: verum end; assume A7: L .: is C_Lattice ; ::_thesis: L is C_Lattice now__::_thesis:_for_p_being_Element_of_L_ex_r_being_Element_of_L_st_r_is_a_complement_of_p let p be Element of L; ::_thesis: ex r being Element of L st r is_a_complement_of p consider q9 being Element of (L .:) such that A8: q9 is_a_complement_of p .: by A7, LATTICES:def_19; q9 "\/" (p .:) = Top (L .:) by A8, LATTICES:def_18; then A9: (.: q9) "/\" p = Top (L .:) ; take r = .: q9; ::_thesis: r is_a_complement_of p L is upper-bounded by A7, LATTICE2:49; then A10: Bottom (L .:) = Top L by LATTICE2:62; q9 "/\" (p .:) = Bottom (L .:) by A8, LATTICES:def_18; then A11: (.: q9) "\/" p = Bottom (L .:) ; L is lower-bounded by A7, LATTICE2:48; then Top (L .:) = Bottom L by LATTICE2:61; hence r is_a_complement_of p by A9, A11, A10, LATTICES:def_18; ::_thesis: verum end; hence L is C_Lattice by A2, A1, A7, LATTICES:def_19; ::_thesis: verum end; theorem Th53: :: FILTER_2:53 for L being Lattice holds ( L is B_Lattice iff L .: is B_Lattice ) proof let L be Lattice; ::_thesis: ( L is B_Lattice iff L .: is B_Lattice ) A1: ( L is distributive iff L .: is distributive ) by LATTICE2:50; ( L is C_Lattice iff L .: is C_Lattice ) by Th52; hence ( L is B_Lattice iff L .: is B_Lattice ) by A1; ::_thesis: verum end; registration let B be B_Lattice; clusterB .: -> Lattice-like Boolean ; coherence ( B .: is Boolean & B .: is Lattice-like ) by Th53; end; Lm4: for B being B_Lattice for a being Element of B holds (a .:) ` = a ` proof let B be B_Lattice; ::_thesis: for a being Element of B holds (a .:) ` = a ` let a be Element of B; ::_thesis: (a .:) ` = a ` ((a .:) `) "/\" (a .:) = Bottom (B .:) by LATTICES:20; then A1: (.: ((a .:) `)) "\/" (.: (a .:)) = Top B by LATTICE2:62; ((a .:) `) "\/" (a .:) = Top (B .:) by LATTICES:21; then (.: ((a .:) `)) "/\" (.: (a .:)) = Bottom B by LATTICE2:61; then .: ((a .:) `) is_a_complement_of a by A1, LATTICES:def_18; hence (a .:) ` = a ` by LATTICES:def_21; ::_thesis: verum end; theorem Th54: :: FILTER_2:54 for B being B_Lattice for a being Element of B for a9 being Element of (B .:) holds ( (a .:) ` = a ` & (.: a9) ` = a9 ` ) proof let B be B_Lattice; ::_thesis: for a being Element of B for a9 being Element of (B .:) holds ( (a .:) ` = a ` & (.: a9) ` = a9 ` ) let a be Element of B; ::_thesis: for a9 being Element of (B .:) holds ( (a .:) ` = a ` & (.: a9) ` = a9 ` ) let a9 be Element of (B .:); ::_thesis: ( (a .:) ` = a ` & (.: a9) ` = a9 ` ) (.: a9) .: = .: a9 ; hence ( (a .:) ` = a ` & (.: a9) ` = a9 ` ) by Lm4; ::_thesis: verum end; theorem :: FILTER_2:55 for B being B_Lattice for IB, JB being Ideal of B holds (.(IB \/ JB).> = IB "\/" JB proof let B be B_Lattice; ::_thesis: for IB, JB being Ideal of B holds (.(IB \/ JB).> = IB "\/" JB let IB, JB be Ideal of B; ::_thesis: (.(IB \/ JB).> = IB "\/" JB reconsider FB = IB .: , GB = JB .: as Filter of (B .:) ; thus (.(IB \/ JB).> = <.((IB \/ JB) .:).) by Th36 .= FB "/\" GB by FILTER_0:39 .= IB "\/" JB by Th44 ; ::_thesis: verum end; theorem :: FILTER_2:56 for B being B_Lattice for IB being Ideal of B holds ( IB is_max-ideal iff ( IB <> the carrier of B & ( for a being Element of B holds ( a in IB or a ` in IB ) ) ) ) proof let B be B_Lattice; ::_thesis: for IB being Ideal of B holds ( IB is_max-ideal iff ( IB <> the carrier of B & ( for a being Element of B holds ( a in IB or a ` in IB ) ) ) ) let IB be Ideal of B; ::_thesis: ( IB is_max-ideal iff ( IB <> the carrier of B & ( for a being Element of B holds ( a in IB or a ` in IB ) ) ) ) reconsider FB = IB .: as Filter of (B .:) ; A1: ( FB is being_ultrafilter iff ( FB <> H1(B .: ) & ( for a being Element of (B .:) holds ( a in FB or a ` in FB ) ) ) ) by FILTER_0:44; thus ( IB is_max-ideal implies ( IB <> H1(B) & ( for a being Element of B holds ( a in IB or a ` in IB ) ) ) ) ::_thesis: ( IB <> the carrier of B & ( for a being Element of B holds ( a in IB or a ` in IB ) ) implies IB is_max-ideal ) proof assume A2: IB is_max-ideal ; ::_thesis: ( IB <> H1(B) & ( for a being Element of B holds ( a in IB or a ` in IB ) ) ) hence IB <> H1(B) by A1, Th32; ::_thesis: for a being Element of B holds ( a in IB or a ` in IB ) let a be Element of B; ::_thesis: ( a in IB or a ` in IB ) reconsider b = a as Element of (B .:) ; ( b in FB or ( b ` in FB & (a .:) ` = a ` ) ) by A1, A2, Th32, Th54; hence ( a in IB or a ` in IB ) ; ::_thesis: verum end; assume that A3: IB <> H1(B) and A4: for a being Element of B holds ( a in IB or a ` in IB ) ; ::_thesis: IB is_max-ideal now__::_thesis:_for_a_being_Element_of_(B_.:)_holds_ (_a_in_FB_or_a_`_in_FB_) let a be Element of (B .:); ::_thesis: ( a in FB or a ` in FB ) reconsider b = a as Element of B ; ( b in FB or ( b ` in FB & (.: a) ` = a ` ) ) by A4, Th54; hence ( a in FB or a ` in FB ) ; ::_thesis: verum end; hence IB is_max-ideal by A1, A3, Th32; ::_thesis: verum end; theorem :: FILTER_2:57 for B being B_Lattice for IB being Ideal of B holds ( ( IB <> (.B.> & IB is prime ) iff IB is_max-ideal ) proof let B be B_Lattice; ::_thesis: for IB being Ideal of B holds ( ( IB <> (.B.> & IB is prime ) iff IB is_max-ideal ) let IB be Ideal of B; ::_thesis: ( ( IB <> (.B.> & IB is prime ) iff IB is_max-ideal ) reconsider F = IB .: as Filter of (B .:) ; <.(B .:).) = (.B.> ; then ( ( F <> (.B.> & F is prime ) iff F is being_ultrafilter ) by FILTER_0:45; hence ( ( IB <> (.B.> & IB is prime ) iff IB is_max-ideal ) by Th32, Th43; ::_thesis: verum end; theorem :: FILTER_2:58 for B being B_Lattice for IB being Ideal of B st IB is_max-ideal holds for a being Element of B holds ( a in IB iff not a ` in IB ) proof let B be B_Lattice; ::_thesis: for IB being Ideal of B st IB is_max-ideal holds for a being Element of B holds ( a in IB iff not a ` in IB ) let IB be Ideal of B; ::_thesis: ( IB is_max-ideal implies for a being Element of B holds ( a in IB iff not a ` in IB ) ) reconsider FB = IB .: as Filter of (B .:) ; assume IB is_max-ideal ; ::_thesis: for a being Element of B holds ( a in IB iff not a ` in IB ) then A1: FB is being_ultrafilter by Th32; let a be Element of B; ::_thesis: ( a in IB iff not a ` in IB ) (a .:) ` = a ` by Lm4; hence ( a in IB iff not a ` in IB ) by A1, FILTER_0:46; ::_thesis: verum end; theorem :: FILTER_2:59 for B being B_Lattice for a, b being Element of B st a <> b holds ex IB being Ideal of B st ( IB is_max-ideal & ( ( a in IB & not b in IB ) or ( not a in IB & b in IB ) ) ) proof let B be B_Lattice; ::_thesis: for a, b being Element of B st a <> b holds ex IB being Ideal of B st ( IB is_max-ideal & ( ( a in IB & not b in IB ) or ( not a in IB & b in IB ) ) ) let a, b be Element of B; ::_thesis: ( a <> b implies ex IB being Ideal of B st ( IB is_max-ideal & ( ( a in IB & not b in IB ) or ( not a in IB & b in IB ) ) ) ) assume a <> b ; ::_thesis: ex IB being Ideal of B st ( IB is_max-ideal & ( ( a in IB & not b in IB ) or ( not a in IB & b in IB ) ) ) then consider FB being Filter of (B .:) such that A1: FB is being_ultrafilter and A2: ( ( a .: in FB & not b .: in FB ) or ( not a .: in FB & b .: in FB ) ) by FILTER_0:47; take IB = .: FB; ::_thesis: ( IB is_max-ideal & ( ( a in IB & not b in IB ) or ( not a in IB & b in IB ) ) ) IB .: = FB ; hence IB is_max-ideal by A1, Th32; ::_thesis: ( ( a in IB & not b in IB ) or ( not a in IB & b in IB ) ) thus ( ( a in IB & not b in IB ) or ( not a in IB & b in IB ) ) by A2; ::_thesis: verum end; theorem Th60: :: FILTER_2:60 for L being Lattice for P being non empty ClosedSubset of L holds ( the L_join of L || P is BinOp of P & the L_meet of L || P is BinOp of P ) proof let L be Lattice; ::_thesis: for P being non empty ClosedSubset of L holds ( the L_join of L || P is BinOp of P & the L_meet of L || P is BinOp of P ) let P be non empty ClosedSubset of L; ::_thesis: ( the L_join of L || P is BinOp of P & the L_meet of L || P is BinOp of P ) dom H2(L) = [:H1(L),H1(L):] by FUNCT_2:def_1; then A1: dom (H2(L) || P) = [:P,P:] by RELAT_1:62; rng (H2(L) || P) c= P proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (H2(L) || P) or x in P ) assume x in rng (H2(L) || P) ; ::_thesis: x in P then consider y being set such that A2: y in [:P,P:] and A3: x = (H2(L) || P) . y by A1, FUNCT_1:def_3; consider p1, p2 being Element of P such that A4: y = [p1,p2] by A2, DOMAIN_1:1; x = p1 "\/" p2 by A1, A3, A4, FUNCT_1:47; hence x in P by LATTICES:def_25; ::_thesis: verum end; hence H2(L) || P is BinOp of P by A1, FUNCT_2:def_1, RELSET_1:4; ::_thesis: the L_meet of L || P is BinOp of P dom H3(L) = [:H1(L),H1(L):] by FUNCT_2:def_1; then A5: dom (H3(L) || P) = [:P,P:] by RELAT_1:62; rng (H3(L) || P) c= P proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (H3(L) || P) or x in P ) assume x in rng (H3(L) || P) ; ::_thesis: x in P then consider y being set such that A6: y in [:P,P:] and A7: x = (H3(L) || P) . y by A5, FUNCT_1:def_3; consider p1, p2 being Element of P such that A8: y = [p1,p2] by A6, DOMAIN_1:1; x = p1 "/\" p2 by A5, A7, A8, FUNCT_1:47; hence x in P by LATTICES:def_24; ::_thesis: verum end; hence the L_meet of L || P is BinOp of P by A5, FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum end; theorem Th61: :: FILTER_2:61 for L being Lattice for P being non empty ClosedSubset of L for o1, o2 being BinOp of P st o1 = the L_join of L || P & o2 = the L_meet of L || P holds ( o1 is commutative & o1 is associative & o2 is commutative & o2 is associative & o1 absorbs o2 & o2 absorbs o1 ) proof let L be Lattice; ::_thesis: for P being non empty ClosedSubset of L for o1, o2 being BinOp of P st o1 = the L_join of L || P & o2 = the L_meet of L || P holds ( o1 is commutative & o1 is associative & o2 is commutative & o2 is associative & o1 absorbs o2 & o2 absorbs o1 ) let P be non empty ClosedSubset of L; ::_thesis: for o1, o2 being BinOp of P st o1 = the L_join of L || P & o2 = the L_meet of L || P holds ( o1 is commutative & o1 is associative & o2 is commutative & o2 is associative & o1 absorbs o2 & o2 absorbs o1 ) let o1, o2 be BinOp of P; ::_thesis: ( o1 = the L_join of L || P & o2 = the L_meet of L || P implies ( o1 is commutative & o1 is associative & o2 is commutative & o2 is associative & o1 absorbs o2 & o2 absorbs o1 ) ) ( H2(L) absorbs H3(L) & H3(L) absorbs H2(L) ) by LATTICE2:26, LATTICE2:27; hence ( o1 = the L_join of L || P & o2 = the L_meet of L || P implies ( o1 is commutative & o1 is associative & o2 is commutative & o2 is associative & o1 absorbs o2 & o2 absorbs o1 ) ) by Th1, Th5; ::_thesis: verum end; definition let L be Lattice; let p, q be Element of L; assume A1: p [= q ; func[#p,q#] -> non empty ClosedSubset of L equals :Def12: :: FILTER_2:def 12 { r where r is Element of L : ( p [= r & r [= q ) } ; coherence { r where r is Element of L : ( p [= r & r [= q ) } is non empty ClosedSubset of L proof set P = { r where r is Element of L : ( p [= r & r [= q ) } ; p in { r where r is Element of L : ( p [= r & r [= q ) } by A1; then reconsider P = { r where r is Element of L : ( p [= r & r [= q ) } as non empty set ; P c= H1(L) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P or x in H1(L) ) assume x in P ; ::_thesis: x in H1(L) then ex r being Element of L st ( x = r & p [= r & r [= q ) ; hence x in H1(L) ; ::_thesis: verum end; then reconsider P = P as non empty Subset of L ; now__::_thesis:_for_p1,_p2_being_Element_of_L_st_p1_in_P_&_p2_in_P_holds_ (_p1_"/\"_p2_in_P_&_p1_"\/"_p2_in_P_) let p1, p2 be Element of L; ::_thesis: ( p1 in P & p2 in P implies ( p1 "/\" p2 in P & p1 "\/" p2 in P ) ) assume that A2: p1 in P and A3: p2 in P ; ::_thesis: ( p1 "/\" p2 in P & p1 "\/" p2 in P ) A4: ex r being Element of L st ( p1 = r & p [= r & r [= q ) by A2; then A5: ( p [= p1 "\/" p2 & p1 "/\" p2 [= q ) by FILTER_0:2, FILTER_0:3; ex r being Element of L st ( p2 = r & p [= r & r [= q ) by A3; then ( p [= p1 "/\" p2 & p1 "\/" p2 [= q ) by A4, FILTER_0:6, FILTER_0:7; hence ( p1 "/\" p2 in P & p1 "\/" p2 in P ) by A5; ::_thesis: verum end; then ( ( for p1, p2 being Element of L st p1 in P & p2 in P holds p1 "/\" p2 in P ) & ( for p1, p2 being Element of L st p1 in P & p2 in P holds p1 "\/" p2 in P ) ) ; hence { r where r is Element of L : ( p [= r & r [= q ) } is non empty ClosedSubset of L by LATTICES:def_24, LATTICES:def_25; ::_thesis: verum end; end; :: deftheorem Def12 defines [# FILTER_2:def_12_:_ for L being Lattice for p, q being Element of L st p [= q holds [#p,q#] = { r where r is Element of L : ( p [= r & r [= q ) } ; theorem Th62: :: FILTER_2:62 for L being Lattice for p, q, r being Element of L st p [= q holds ( r in [#p,q#] iff ( p [= r & r [= q ) ) proof let L be Lattice; ::_thesis: for p, q, r being Element of L st p [= q holds ( r in [#p,q#] iff ( p [= r & r [= q ) ) let p, q, r be Element of L; ::_thesis: ( p [= q implies ( r in [#p,q#] iff ( p [= r & r [= q ) ) ) assume p [= q ; ::_thesis: ( r in [#p,q#] iff ( p [= r & r [= q ) ) then [#p,q#] = { s where s is Element of L : ( p [= s & s [= q ) } by Def12; then ( r in [#p,q#] iff ex s being Element of L st ( r = s & p [= s & s [= q ) ) ; hence ( r in [#p,q#] iff ( p [= r & r [= q ) ) ; ::_thesis: verum end; theorem :: FILTER_2:63 for L being Lattice for p, q being Element of L st p [= q holds ( p in [#p,q#] & q in [#p,q#] ) by Th62; theorem :: FILTER_2:64 for L being Lattice for p being Element of L holds [#p,p#] = {p} proof let L be Lattice; ::_thesis: for p being Element of L holds [#p,p#] = {p} let p be Element of L; ::_thesis: [#p,p#] = {p} let q be Element of L; :: according to FILTER_2:def_1 ::_thesis: ( q in [#p,p#] iff q in {p} ) hereby ::_thesis: ( q in {p} implies q in [#p,p#] ) assume q in [#p,p#] ; ::_thesis: q in {p} then ( p [= q & q [= p ) by Th62; then q = p by LATTICES:8; hence q in {p} by TARSKI:def_1; ::_thesis: verum end; p in [#p,p#] by Th62; hence ( q in {p} implies q in [#p,p#] ) by TARSKI:def_1; ::_thesis: verum end; theorem :: FILTER_2:65 for L being Lattice for p being Element of L st L is upper-bounded holds <.p.) = [#p,(Top L)#] proof let L be Lattice; ::_thesis: for p being Element of L st L is upper-bounded holds <.p.) = [#p,(Top L)#] let p be Element of L; ::_thesis: ( L is upper-bounded implies <.p.) = [#p,(Top L)#] ) assume A1: L is upper-bounded ; ::_thesis: <.p.) = [#p,(Top L)#] let q be Element of L; :: according to FILTER_2:def_1 ::_thesis: ( q in <.p.) iff q in [#p,(Top L)#] ) A2: ( q in <.p.) iff p [= q ) by FILTER_0:15; ( p [= Top L & q [= Top L ) by A1, LATTICES:19; hence ( q in <.p.) iff q in [#p,(Top L)#] ) by A2, Th62; ::_thesis: verum end; theorem :: FILTER_2:66 for L being Lattice for p being Element of L st L is lower-bounded holds (.p.> = [#(Bottom L),p#] proof let L be Lattice; ::_thesis: for p being Element of L st L is lower-bounded holds (.p.> = [#(Bottom L),p#] let p be Element of L; ::_thesis: ( L is lower-bounded implies (.p.> = [#(Bottom L),p#] ) assume A1: L is lower-bounded ; ::_thesis: (.p.> = [#(Bottom L),p#] let q be Element of L; :: according to FILTER_2:def_1 ::_thesis: ( q in (.p.> iff q in [#(Bottom L),p#] ) A2: ( q in (.p.> iff q [= p ) by Th28; ( Bottom L [= p & Bottom L [= q ) by A1, LATTICES:16; hence ( q in (.p.> iff q in [#(Bottom L),p#] ) by A2, Th62; ::_thesis: verum end; theorem :: FILTER_2:67 for L1, L2 being Lattice for F1 being Filter of L1 for F2 being Filter of L2 st LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) & F1 = F2 holds latt F1 = latt F2 proof let L1, L2 be Lattice; ::_thesis: for F1 being Filter of L1 for F2 being Filter of L2 st LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) & F1 = F2 holds latt F1 = latt F2 let F1 be Filter of L1; ::_thesis: for F2 being Filter of L2 st LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) & F1 = F2 holds latt F1 = latt F2 let F2 be Filter of L2; ::_thesis: ( LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) & F1 = F2 implies latt F1 = latt F2 ) ex o1, o2 being BinOp of F1 st ( o1 = the L_join of L1 || F1 & o2 = the L_meet of L1 || F1 & latt F1 = LattStr(# F1,o1,o2 #) ) by FILTER_0:def_9; hence ( LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) & F1 = F2 implies latt F1 = latt F2 ) by FILTER_0:def_9; ::_thesis: verum end; begin notation let L be Lattice; synonym Sublattice of L for SubLattice of L; end; definition let L be Lattice; redefine mode SubLattice of L means :Def13: :: FILTER_2:def 13 ex P being non empty ClosedSubset of L ex o1, o2 being BinOp of P st ( o1 = the L_join of L || P & o2 = the L_meet of L || P & LattStr(# the carrier of it, the L_join of it, the L_meet of it #) = LattStr(# P,o1,o2 #) ); compatibility for b1 being LattStr holds ( b1 is Sublattice of L iff ex P being non empty ClosedSubset of L ex o1, o2 being BinOp of P st ( o1 = the L_join of L || P & o2 = the L_meet of L || P & LattStr(# the carrier of b1, the L_join of b1, the L_meet of b1 #) = LattStr(# P,o1,o2 #) ) ) proof let K be Lattice; ::_thesis: ( K is Sublattice of L iff ex P being non empty ClosedSubset of L ex o1, o2 being BinOp of P st ( o1 = the L_join of L || P & o2 = the L_meet of L || P & LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# P,o1,o2 #) ) ) thus ( K is SubLattice of L implies ex P being non empty ClosedSubset of L ex o1, o2 being BinOp of P st ( o1 = the L_join of L || P & o2 = the L_meet of L || P & LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# P,o1,o2 #) ) ) ::_thesis: ( ex P being non empty ClosedSubset of L ex o1, o2 being BinOp of P st ( o1 = the L_join of L || P & o2 = the L_meet of L || P & LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# P,o1,o2 #) ) implies K is Sublattice of L ) proof assume A1: K is SubLattice of L ; ::_thesis: ex P being non empty ClosedSubset of L ex o1, o2 being BinOp of P st ( o1 = the L_join of L || P & o2 = the L_meet of L || P & LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# P,o1,o2 #) ) then A2: H3(K) = H3(L) || H1(K) by NAT_LAT:def_12; reconsider P = H1(K) as non empty Subset of L by A1, NAT_LAT:def_12; A3: H2(K) = H2(L) || H1(K) by A1, NAT_LAT:def_12; now__::_thesis:_for_p,_q_being_Element_of_L_st_p_in_P_&_q_in_P_holds_ (_p_"/\"_q_in_P_&_p_"\/"_q_in_P_) let p, q be Element of L; ::_thesis: ( p in P & q in P implies ( p "/\" q in P & p "\/" q in P ) ) assume ( p in P & q in P ) ; ::_thesis: ( p "/\" q in P & p "\/" q in P ) then A4: [p,q] in [:P,P:] by ZFMISC_1:87; dom H3(K) = [:P,P:] by FUNCT_2:def_1; then A5: H3(L) . [p,q] = H3(K) . [p,q] by A2, A4, FUNCT_1:47; dom H2(K) = [:P,P:] by FUNCT_2:def_1; then H2(L) . [p,q] = H2(K) . [p,q] by A3, A4, FUNCT_1:47; hence ( p "/\" q in P & p "\/" q in P ) by A4, A5, FUNCT_2:5; ::_thesis: verum end; then ( ( for p1, p2 being Element of L st p1 in P & p2 in P holds p1 "/\" p2 in P ) & ( for p1, p2 being Element of L st p1 in P & p2 in P holds p1 "\/" p2 in P ) ) ; then reconsider P = P as non empty ClosedSubset of L by LATTICES:def_24, LATTICES:def_25; take P ; ::_thesis: ex o1, o2 being BinOp of P st ( o1 = the L_join of L || P & o2 = the L_meet of L || P & LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# P,o1,o2 #) ) reconsider o1 = H2(K), o2 = H3(K) as BinOp of P ; take o1 ; ::_thesis: ex o2 being BinOp of P st ( o1 = the L_join of L || P & o2 = the L_meet of L || P & LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# P,o1,o2 #) ) take o2 ; ::_thesis: ( o1 = the L_join of L || P & o2 = the L_meet of L || P & LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# P,o1,o2 #) ) thus ( o1 = the L_join of L || P & o2 = the L_meet of L || P & LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# P,o1,o2 #) ) by A1, NAT_LAT:def_12; ::_thesis: verum end; given P being non empty ClosedSubset of L, o1, o2 being BinOp of P such that A6: ( o1 = the L_join of L || P & o2 = the L_meet of L || P & LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# P,o1,o2 #) ) ; ::_thesis: K is Sublattice of L thus K is Sublattice of L by A6, NAT_LAT:def_12; ::_thesis: verum end; end; :: deftheorem Def13 defines Sublattice FILTER_2:def_13_:_ for L being Lattice for b2 being LattStr holds ( b2 is Sublattice of L iff ex P being non empty ClosedSubset of L ex o1, o2 being BinOp of P st ( o1 = the L_join of L || P & o2 = the L_meet of L || P & LattStr(# the carrier of b2, the L_join of b2, the L_meet of b2 #) = LattStr(# P,o1,o2 #) ) ); theorem Th68: :: FILTER_2:68 for L being Lattice for K being Sublattice of L for a being Element of K holds a is Element of L proof let L be Lattice; ::_thesis: for K being Sublattice of L for a being Element of K holds a is Element of L let K be Sublattice of L; ::_thesis: for a being Element of K holds a is Element of L H1(K) c= H1(L) by NAT_LAT:def_12; hence for a being Element of K holds a is Element of L by TARSKI:def_3; ::_thesis: verum end; definition let L be Lattice; let P be non empty ClosedSubset of L; func latt (L,P) -> Sublattice of L means :Def14: :: FILTER_2:def 14 ex o1, o2 being BinOp of P st ( o1 = the L_join of L || P & o2 = the L_meet of L || P & it = LattStr(# P,o1,o2 #) ); existence ex b1 being Sublattice of L ex o1, o2 being BinOp of P st ( o1 = the L_join of L || P & o2 = the L_meet of L || P & b1 = LattStr(# P,o1,o2 #) ) proof reconsider o1 = H2(L) || P, o2 = H3(L) || P as BinOp of P by Th60; o1 = H2(L) || P ; then A1: ( o2 is commutative & o2 is associative ) by Th61; o2 = H3(L) || P ; then A2: ( o1 is commutative & o1 is associative ) by Th61; ( o1 absorbs o2 & o2 absorbs o1 ) by Th61; then reconsider K = LattStr(# P,o1,o2 #) as strict Lattice by A2, A1, LATTICE2:11; reconsider K = K as strict Sublattice of L by NAT_LAT:def_12; take K ; ::_thesis: ex o1, o2 being BinOp of P st ( o1 = the L_join of L || P & o2 = the L_meet of L || P & K = LattStr(# P,o1,o2 #) ) take o1 ; ::_thesis: ex o2 being BinOp of P st ( o1 = the L_join of L || P & o2 = the L_meet of L || P & K = LattStr(# P,o1,o2 #) ) take o2 ; ::_thesis: ( o1 = the L_join of L || P & o2 = the L_meet of L || P & K = LattStr(# P,o1,o2 #) ) thus ( o1 = the L_join of L || P & o2 = the L_meet of L || P & K = LattStr(# P,o1,o2 #) ) ; ::_thesis: verum end; uniqueness for b1, b2 being Sublattice of L st ex o1, o2 being BinOp of P st ( o1 = the L_join of L || P & o2 = the L_meet of L || P & b1 = LattStr(# P,o1,o2 #) ) & ex o1, o2 being BinOp of P st ( o1 = the L_join of L || P & o2 = the L_meet of L || P & b2 = LattStr(# P,o1,o2 #) ) holds b1 = b2 ; end; :: deftheorem Def14 defines latt FILTER_2:def_14_:_ for L being Lattice for P being non empty ClosedSubset of L for b3 being Sublattice of L holds ( b3 = latt (L,P) iff ex o1, o2 being BinOp of P st ( o1 = the L_join of L || P & o2 = the L_meet of L || P & b3 = LattStr(# P,o1,o2 #) ) ); registration let L be Lattice; let P be non empty ClosedSubset of L; cluster latt (L,P) -> strict ; coherence latt (L,P) is strict proof ex o1, o2 being BinOp of P st ( o1 = the L_join of L || P & o2 = the L_meet of L || P & latt (L,P) = LattStr(# P,o1,o2 #) ) by Def14; hence latt (L,P) is strict ; ::_thesis: verum end; end; definition let L be Lattice; let l be Sublattice of L; :: original: .: redefine funcl .: -> strict Sublattice of L .: ; coherence l .: is strict Sublattice of L .: proof consider P being non empty ClosedSubset of L, o1, o2 being BinOp of P such that A1: ( o1 = H2(L) || P & o2 = H3(L) || P & LattStr(# the carrier of l, the L_join of l, the L_meet of l #) = LattStr(# P,o1,o2 #) ) by Def13; l .: is Sublattice of L .: proof take P .: ; :: according to FILTER_2:def_13 ::_thesis: ex o1, o2 being BinOp of (P .:) st ( o1 = the L_join of (L .:) || (P .:) & o2 = the L_meet of (L .:) || (P .:) & LattStr(# the carrier of (l .:), the L_join of (l .:), the L_meet of (l .:) #) = LattStr(# (P .:),o1,o2 #) ) thus ex o1, o2 being BinOp of (P .:) st ( o1 = the L_join of (L .:) || (P .:) & o2 = the L_meet of (L .:) || (P .:) & LattStr(# the carrier of (l .:), the L_join of (l .:), the L_meet of (l .:) #) = LattStr(# (P .:),o1,o2 #) ) by A1; ::_thesis: verum end; hence l .: is strict Sublattice of L .: ; ::_thesis: verum end; end; theorem Th69: :: FILTER_2:69 for L being Lattice for F being Filter of L holds latt F = latt (L,F) proof let L be Lattice; ::_thesis: for F being Filter of L holds latt F = latt (L,F) let F be Filter of L; ::_thesis: latt F = latt (L,F) ex o1, o2 being BinOp of F st ( o1 = H2(L) || F & o2 = H3(L) || F & latt (L,F) = LattStr(# F,o1,o2 #) ) by Def14; hence latt F = latt (L,F) by FILTER_0:def_9; ::_thesis: verum end; theorem Th70: :: FILTER_2:70 for L being Lattice for P being non empty ClosedSubset of L holds latt (L,P) = (latt ((L .:),(P .:))) .: proof let L be Lattice; ::_thesis: for P being non empty ClosedSubset of L holds latt (L,P) = (latt ((L .:),(P .:))) .: let P be non empty ClosedSubset of L; ::_thesis: latt (L,P) = (latt ((L .:),(P .:))) .: ( ex o1, o2 being BinOp of P st ( o1 = H2(L) || P & o2 = H3(L) || P & latt (L,P) = LattStr(# P,o1,o2 #) ) & ex o3, o4 being BinOp of (P .:) st ( o3 = H2(L .: ) || (P .:) & o4 = H3(L .: ) || (P .:) & latt ((L .:),(P .:)) = LattStr(# (P .:),o3,o4 #) ) ) by Def14; hence latt (L,P) = (latt ((L .:),(P .:))) .: ; ::_thesis: verum end; theorem :: FILTER_2:71 for L being Lattice holds ( latt (L,(.L.>) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) & latt (L,<.L.)) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) ) proof let L be Lattice; ::_thesis: ( latt (L,(.L.>) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) & latt (L,<.L.)) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) ) A1: ( dom H3(L) = [:H1(L),H1(L):] & H2(L) | (dom H2(L)) = H2(L) ) by FUNCT_2:def_1, RELAT_1:68; ( ex o1, o2 being BinOp of (.L.> st ( o1 = the L_join of L || (.L.> & o2 = the L_meet of L || (.L.> & latt (L,(.L.>) = LattStr(# (.L.>,o1,o2 #) ) & dom H2(L) = [:H1(L),H1(L):] ) by Def14, FUNCT_2:def_1; hence ( latt (L,(.L.>) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) & latt (L,<.L.)) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) ) by A1, RELAT_1:68; ::_thesis: verum end; theorem Th72: :: FILTER_2:72 for L being Lattice for P being non empty ClosedSubset of L holds ( the carrier of (latt (L,P)) = P & the L_join of (latt (L,P)) = the L_join of L || P & the L_meet of (latt (L,P)) = the L_meet of L || P ) proof let L be Lattice; ::_thesis: for P being non empty ClosedSubset of L holds ( the carrier of (latt (L,P)) = P & the L_join of (latt (L,P)) = the L_join of L || P & the L_meet of (latt (L,P)) = the L_meet of L || P ) let P be non empty ClosedSubset of L; ::_thesis: ( the carrier of (latt (L,P)) = P & the L_join of (latt (L,P)) = the L_join of L || P & the L_meet of (latt (L,P)) = the L_meet of L || P ) ex o1, o2 being BinOp of P st ( o1 = H2(L) || P & o2 = H3(L) || P & latt (L,P) = LattStr(# P,o1,o2 #) ) by Def14; hence ( the carrier of (latt (L,P)) = P & the L_join of (latt (L,P)) = the L_join of L || P & the L_meet of (latt (L,P)) = the L_meet of L || P ) ; ::_thesis: verum end; theorem Th73: :: FILTER_2:73 for L being Lattice for P being non empty ClosedSubset of L for p, q being Element of L for p9, q9 being Element of (latt (L,P)) st p = p9 & q = q9 holds ( p "\/" q = p9 "\/" q9 & p "/\" q = p9 "/\" q9 ) proof let L be Lattice; ::_thesis: for P being non empty ClosedSubset of L for p, q being Element of L for p9, q9 being Element of (latt (L,P)) st p = p9 & q = q9 holds ( p "\/" q = p9 "\/" q9 & p "/\" q = p9 "/\" q9 ) let P be non empty ClosedSubset of L; ::_thesis: for p, q being Element of L for p9, q9 being Element of (latt (L,P)) st p = p9 & q = q9 holds ( p "\/" q = p9 "\/" q9 & p "/\" q = p9 "/\" q9 ) let p, q be Element of L; ::_thesis: for p9, q9 being Element of (latt (L,P)) st p = p9 & q = q9 holds ( p "\/" q = p9 "\/" q9 & p "/\" q = p9 "/\" q9 ) let p9, q9 be Element of (latt (L,P)); ::_thesis: ( p = p9 & q = q9 implies ( p "\/" q = p9 "\/" q9 & p "/\" q = p9 "/\" q9 ) ) assume A1: ( p = p9 & q = q9 ) ; ::_thesis: ( p "\/" q = p9 "\/" q9 & p "/\" q = p9 "/\" q9 ) consider o1, o2 being BinOp of P such that A2: o1 = H2(L) || P and A3: o2 = H3(L) || P and A4: latt (L,P) = LattStr(# P,o1,o2 #) by Def14; A5: [p9,q9] in [:P,P:] by A4; dom o1 = [:P,P:] by FUNCT_2:def_1; hence p "\/" q = p9 "\/" q9 by A1, A2, A4, A5, FUNCT_1:47; ::_thesis: p "/\" q = p9 "/\" q9 dom o2 = [:P,P:] by FUNCT_2:def_1; hence p "/\" q = p9 "/\" q9 by A1, A3, A4, A5, FUNCT_1:47; ::_thesis: verum end; theorem Th74: :: FILTER_2:74 for L being Lattice for P being non empty ClosedSubset of L for p, q being Element of L for p9, q9 being Element of (latt (L,P)) st p = p9 & q = q9 holds ( p [= q iff p9 [= q9 ) proof let L be Lattice; ::_thesis: for P being non empty ClosedSubset of L for p, q being Element of L for p9, q9 being Element of (latt (L,P)) st p = p9 & q = q9 holds ( p [= q iff p9 [= q9 ) let P be non empty ClosedSubset of L; ::_thesis: for p, q being Element of L for p9, q9 being Element of (latt (L,P)) st p = p9 & q = q9 holds ( p [= q iff p9 [= q9 ) let p, q be Element of L; ::_thesis: for p9, q9 being Element of (latt (L,P)) st p = p9 & q = q9 holds ( p [= q iff p9 [= q9 ) let p9, q9 be Element of (latt (L,P)); ::_thesis: ( p = p9 & q = q9 implies ( p [= q iff p9 [= q9 ) ) assume A1: ( p = p9 & q = q9 ) ; ::_thesis: ( p [= q iff p9 [= q9 ) thus ( p [= q implies p9 [= q9 ) ::_thesis: ( p9 [= q9 implies p [= q ) proof assume p "\/" q = q ; :: according to LATTICES:def_3 ::_thesis: p9 [= q9 hence p9 "\/" q9 = q9 by A1, Th73; :: according to LATTICES:def_3 ::_thesis: verum end; assume p9 "\/" q9 = q9 ; :: according to LATTICES:def_3 ::_thesis: p [= q hence p "\/" q = q by A1, Th73; :: according to LATTICES:def_3 ::_thesis: verum end; theorem :: FILTER_2:75 for L being Lattice for I being Ideal of L st L is lower-bounded holds latt (L,I) is lower-bounded proof let L be Lattice; ::_thesis: for I being Ideal of L st L is lower-bounded holds latt (L,I) is lower-bounded let I be Ideal of L; ::_thesis: ( L is lower-bounded implies latt (L,I) is lower-bounded ) set b9 = the Element of (latt (L,I)); reconsider b = the Element of (latt (L,I)) as Element of L by Th68; given c being Element of L such that A1: for a being Element of L holds ( c "/\" a = c & a "/\" c = c ) ; :: according to LATTICES:def_13 ::_thesis: latt (L,I) is lower-bounded A2: H1( latt (L,I)) = I by Th72; c "/\" b = c by A1; then reconsider c9 = c as Element of (latt (L,I)) by A2, Th22; take c9 ; :: according to LATTICES:def_13 ::_thesis: for b1 being Element of the carrier of (latt (L,I)) holds ( c9 "/\" b1 = c9 & b1 "/\" c9 = c9 ) let a9 be Element of (latt (L,I)); ::_thesis: ( c9 "/\" a9 = c9 & a9 "/\" c9 = c9 ) reconsider a = a9 as Element of L by Th68; thus c9 "/\" a9 = c "/\" a by Th73 .= c9 by A1 ; ::_thesis: a9 "/\" c9 = c9 hence a9 "/\" c9 = c9 ; ::_thesis: verum end; theorem :: FILTER_2:76 for L being Lattice for P being non empty ClosedSubset of L st L is modular holds latt (L,P) is modular proof let L be Lattice; ::_thesis: for P being non empty ClosedSubset of L st L is modular holds latt (L,P) is modular let P be non empty ClosedSubset of L; ::_thesis: ( L is modular implies latt (L,P) is modular ) assume A1: for a, b, c being Element of L st a [= c holds a "\/" (b "/\" c) = (a "\/" b) "/\" c ; :: according to LATTICES:def_12 ::_thesis: latt (L,P) is modular let a9, b9, c9 be Element of (latt (L,P)); :: according to LATTICES:def_12 ::_thesis: ( not a9 [= c9 or a9 "\/" (b9 "/\" c9) = (a9 "\/" b9) "/\" c9 ) reconsider a = a9, b = b9, c = c9, bc = b9 "/\" c9, ab = a9 "\/" b9 as Element of L by Th68; assume a9 [= c9 ; ::_thesis: a9 "\/" (b9 "/\" c9) = (a9 "\/" b9) "/\" c9 then A2: a [= c by Th74; thus a9 "\/" (b9 "/\" c9) = a "\/" bc by Th73 .= a "\/" (b "/\" c) by Th73 .= (a "\/" b) "/\" c by A1, A2 .= ab "/\" c by Th73 .= (a9 "\/" b9) "/\" c9 by Th73 ; ::_thesis: verum end; theorem Th77: :: FILTER_2:77 for L being Lattice for P being non empty ClosedSubset of L st L is distributive holds latt (L,P) is distributive proof let L be Lattice; ::_thesis: for P being non empty ClosedSubset of L st L is distributive holds latt (L,P) is distributive let P be non empty ClosedSubset of L; ::_thesis: ( L is distributive implies latt (L,P) is distributive ) assume A1: for a, b, c being Element of L holds a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c) ; :: according to LATTICES:def_11 ::_thesis: latt (L,P) is distributive let a9, b9, c9 be Element of (latt (L,P)); :: according to LATTICES:def_11 ::_thesis: a9 "/\" (b9 "\/" c9) = (a9 "/\" b9) "\/" (a9 "/\" c9) reconsider a = a9, b = b9, c = c9, bc = b9 "\/" c9, ab = a9 "/\" b9, ac = a9 "/\" c9 as Element of L by Th68; thus a9 "/\" (b9 "\/" c9) = a "/\" bc by Th73 .= a "/\" (b "\/" c) by Th73 .= (a "/\" b) "\/" (a "/\" c) by A1 .= ab "\/" (a "/\" c) by Th73 .= ab "\/" ac by Th73 .= (a9 "/\" b9) "\/" (a9 "/\" c9) by Th73 ; ::_thesis: verum end; theorem :: FILTER_2:78 for L being Lattice for p, q being Element of L st L is implicative & p [= q holds latt (L,[#p,q#]) is implicative proof let L be Lattice; ::_thesis: for p, q being Element of L st L is implicative & p [= q holds latt (L,[#p,q#]) is implicative let p, q be Element of L; ::_thesis: ( L is implicative & p [= q implies latt (L,[#p,q#]) is implicative ) assume A1: L is implicative ; ::_thesis: ( not p [= q or latt (L,[#p,q#]) is implicative ) set P = [#p,q#]; set K = latt (L,[#p,q#]); assume A2: p [= q ; ::_thesis: latt (L,[#p,q#]) is implicative let a9, b9 be Element of (latt (L,[#p,q#])); :: according to FILTER_0:def_6 ::_thesis: ex b1 being Element of the carrier of (latt (L,[#p,q#])) st ( a9 "/\" b1 [= b9 & ( for b2 being Element of the carrier of (latt (L,[#p,q#])) holds ( not a9 "/\" b2 [= b9 or b2 [= b1 ) ) ) reconsider a = a9, b = b9 as Element of L by Th68; set c = a => b; A3: H1( latt (L,[#p,q#])) = [#p,q#] by Th72; then p [= a by A2, Th62; then A4: p "\/" ((a => b) "/\" a) = (p "\/" (a => b)) "/\" a by A1, LATTICES:def_12; A5: a "/\" (a => b) [= b by A1, FILTER_0:def_7; p [= b by A2, A3, Th62; then p "\/" (a "/\" (a => b)) [= b by A5, FILTER_0:6; then A6: (p "\/" (a "/\" (a => b))) "/\" q [= b by FILTER_0:2; set d = ((a => b) "\/" p) "/\" q; p [= (a => b) "\/" p by LATTICES:5; then ( ((a => b) "\/" p) "/\" q [= q & p [= ((a => b) "\/" p) "/\" q ) by A2, FILTER_0:7, LATTICES:6; then reconsider d9 = ((a => b) "\/" p) "/\" q as Element of (latt (L,[#p,q#])) by A2, A3, Th62; take d9 ; ::_thesis: ( a9 "/\" d9 [= b9 & ( for b1 being Element of the carrier of (latt (L,[#p,q#])) holds ( not a9 "/\" b1 [= b9 or b1 [= d9 ) ) ) ( ((p "\/" (a => b)) "/\" a) "/\" q = a "/\" (((a => b) "\/" p) "/\" q) & a "/\" (((a => b) "\/" p) "/\" q) = a9 "/\" d9 ) by Th73, LATTICES:def_7; hence a9 "/\" d9 [= b9 by A4, A6, Th74; ::_thesis: for b1 being Element of the carrier of (latt (L,[#p,q#])) holds ( not a9 "/\" b1 [= b9 or b1 [= d9 ) let e9 be Element of (latt (L,[#p,q#])); ::_thesis: ( not a9 "/\" e9 [= b9 or e9 [= d9 ) reconsider e = e9, ae = a9 "/\" e9 as Element of L by Th68; e [= q by A2, A3, Th62; then A7: e = e "/\" q by LATTICES:4; assume a9 "/\" e9 [= b9 ; ::_thesis: e9 [= d9 then ae [= b by Th74; then a "/\" e [= b by Th73; then A8: e [= a => b by A1, FILTER_0:def_7; p [= e by A2, A3, Th62; then e = e "\/" p by LATTICES:def_3; then e [= (a => b) "\/" p by A8, FILTER_0:1; then e [= ((a => b) "\/" p) "/\" q by A7, LATTICES:9; hence e9 [= d9 by Th74; ::_thesis: verum end; registration let L be Lattice; let p be Element of L; cluster latt (L,(.p.>) -> upper-bounded ; coherence latt (L,(.p.>) is upper-bounded proof latt (L,(.p.>) = (latt ((L .:),((.p.> .:))) .: by Th70 .= (latt ((L .:),<.(p .:).))) .: by Th29 .= (latt <.(p .:).)) .: by Th69 ; hence latt (L,(.p.>) is upper-bounded by LATTICE2:48; ::_thesis: verum end; end; theorem Th79: :: FILTER_2:79 for L being Lattice for p being Element of L holds Top (latt (L,(.p.>)) = p proof let L be Lattice; ::_thesis: for p being Element of L holds Top (latt (L,(.p.>)) = p let p be Element of L; ::_thesis: Top (latt (L,(.p.>)) = p latt (L,(.p.>) = (latt ((L .:),((.p.> .:))) .: by Th70 .= (latt ((L .:),<.(p .:).))) .: by Th29 .= (latt <.(p .:).)) .: by Th69 ; hence Top (latt (L,(.p.>)) = Bottom (latt <.(p .:).)) by LATTICE2:61 .= p by FILTER_0:56 ; ::_thesis: verum end; theorem Th80: :: FILTER_2:80 for L being Lattice for p being Element of L st L is lower-bounded holds ( latt (L,(.p.>) is lower-bounded & Bottom (latt (L,(.p.>)) = Bottom L ) proof let L be Lattice; ::_thesis: for p being Element of L st L is lower-bounded holds ( latt (L,(.p.>) is lower-bounded & Bottom (latt (L,(.p.>)) = Bottom L ) let p be Element of L; ::_thesis: ( L is lower-bounded implies ( latt (L,(.p.>) is lower-bounded & Bottom (latt (L,(.p.>)) = Bottom L ) ) assume A1: L is lower-bounded ; ::_thesis: ( latt (L,(.p.>) is lower-bounded & Bottom (latt (L,(.p.>)) = Bottom L ) then A2: L .: is upper-bounded by LATTICE2:48; then A3: latt <.(p .:).) is upper-bounded by FILTER_0:52; A4: latt (L,(.p.>) = (latt ((L .:),((.p.> .:))) .: by Th70 .= (latt ((L .:),<.(p .:).))) .: by Th29 .= (latt <.(p .:).)) .: by Th69 ; hence latt (L,(.p.>) is lower-bounded by A3, LATTICE2:49; ::_thesis: Bottom (latt (L,(.p.>)) = Bottom L Top (latt <.(p .:).)) = Top (L .:) by A2, FILTER_0:57; hence Bottom (latt (L,(.p.>)) = Top (L .:) by A4, A3, LATTICE2:62 .= Bottom L by A1, LATTICE2:61 ; ::_thesis: verum end; theorem Th81: :: FILTER_2:81 for L being Lattice for p being Element of L st L is lower-bounded holds latt (L,(.p.>) is bounded proof let L be Lattice; ::_thesis: for p being Element of L st L is lower-bounded holds latt (L,(.p.>) is bounded let p be Element of L; ::_thesis: ( L is lower-bounded implies latt (L,(.p.>) is bounded ) assume L is lower-bounded ; ::_thesis: latt (L,(.p.>) is bounded then latt (L,(.p.>) is lower-bounded upper-bounded Lattice by Th80; hence latt (L,(.p.>) is bounded ; ::_thesis: verum end; theorem Th82: :: FILTER_2:82 for L being Lattice for p, q being Element of L st p [= q holds ( latt (L,[#p,q#]) is bounded & Top (latt (L,[#p,q#])) = q & Bottom (latt (L,[#p,q#])) = p ) proof let L be Lattice; ::_thesis: for p, q being Element of L st p [= q holds ( latt (L,[#p,q#]) is bounded & Top (latt (L,[#p,q#])) = q & Bottom (latt (L,[#p,q#])) = p ) let p, q be Element of L; ::_thesis: ( p [= q implies ( latt (L,[#p,q#]) is bounded & Top (latt (L,[#p,q#])) = q & Bottom (latt (L,[#p,q#])) = p ) ) assume A1: p [= q ; ::_thesis: ( latt (L,[#p,q#]) is bounded & Top (latt (L,[#p,q#])) = q & Bottom (latt (L,[#p,q#])) = p ) A2: H1( latt (L,[#p,q#])) = [#p,q#] by Th72; then reconsider p9 = p, q9 = q as Element of (latt (L,[#p,q#])) by A1, Th62; A3: now__::_thesis:_for_a9_being_Element_of_(latt_(L,[#p,q#]))_holds_ (_q9_"\/"_a9_=_q9_&_a9_"\/"_q9_=_q9_) let a9 be Element of (latt (L,[#p,q#])); ::_thesis: ( q9 "\/" a9 = q9 & a9 "\/" q9 = q9 ) reconsider a = a9 as Element of L by Th68; A4: a [= q by A1, A2, Th62; thus q9 "\/" a9 = q "\/" a by Th73 .= q9 by A4, LATTICES:def_3 ; ::_thesis: a9 "\/" q9 = q9 hence a9 "\/" q9 = q9 ; ::_thesis: verum end; A5: now__::_thesis:_for_a9_being_Element_of_(latt_(L,[#p,q#]))_holds_ (_p9_"/\"_a9_=_p9_&_a9_"/\"_p9_=_p9_) let a9 be Element of (latt (L,[#p,q#])); ::_thesis: ( p9 "/\" a9 = p9 & a9 "/\" p9 = p9 ) reconsider a = a9 as Element of L by Th68; A6: p [= a by A1, A2, Th62; thus p9 "/\" a9 = p "/\" a by Th73 .= p9 by A6, LATTICES:4 ; ::_thesis: a9 "/\" p9 = p9 hence a9 "/\" p9 = p9 ; ::_thesis: verum end; then A7: latt (L,[#p,q#]) is lower-bounded upper-bounded Lattice by A3, LATTICES:def_13, LATTICES:def_14; hence latt (L,[#p,q#]) is bounded ; ::_thesis: ( Top (latt (L,[#p,q#])) = q & Bottom (latt (L,[#p,q#])) = p ) thus ( Top (latt (L,[#p,q#])) = q & Bottom (latt (L,[#p,q#])) = p ) by A5, A3, A7, LATTICES:def_16, LATTICES:def_17; ::_thesis: verum end; theorem :: FILTER_2:83 for L being Lattice for p being Element of L st L is C_Lattice & L is modular holds latt (L,(.p.>) is C_Lattice proof let L be Lattice; ::_thesis: for p being Element of L st L is C_Lattice & L is modular holds latt (L,(.p.>) is C_Lattice let p be Element of L; ::_thesis: ( L is C_Lattice & L is modular implies latt (L,(.p.>) is C_Lattice ) assume that A1: L is C_Lattice and A2: L is modular ; ::_thesis: latt (L,(.p.>) is C_Lattice reconsider K = latt (L,(.p.>) as bounded Lattice by A1, Th81; K is complemented proof let b9 be Element of K; :: according to LATTICES:def_19 ::_thesis: ex b1 being Element of the carrier of K st b1 is_a_complement_of b9 reconsider b = b9 as Element of L by Th68; consider a being Element of L such that A3: a is_a_complement_of b by A1, LATTICES:def_19; A4: a "\/" b = Top L by A3, LATTICES:def_18; A5: H1(K) = (.p.> by Th72; then A6: b [= p by Th28; p "/\" a [= p by LATTICES:6; then reconsider a9 = p "/\" a as Element of K by A5, Th28; take a9 ; ::_thesis: a9 is_a_complement_of b9 thus a9 "\/" b9 = (p "/\" a) "\/" b by Th73 .= (b "\/" a) "/\" p by A2, A6, LATTICES:def_12 .= p by A1, A4, LATTICES:17 .= Top K by Th79 ; :: according to LATTICES:def_18 ::_thesis: ( b9 "\/" a9 = Top K & a9 "/\" b9 = Bottom K & b9 "/\" a9 = Bottom K ) hence b9 "\/" a9 = Top K ; ::_thesis: ( a9 "/\" b9 = Bottom K & b9 "/\" a9 = Bottom K ) A7: a "/\" b = Bottom L by A3, LATTICES:def_18; thus a9 "/\" b9 = (p "/\" a) "/\" b by Th73 .= p "/\" (Bottom L) by A7, LATTICES:def_7 .= Bottom L by A1 .= Bottom K by A1, Th80 ; ::_thesis: b9 "/\" a9 = Bottom K hence b9 "/\" a9 = Bottom K ; ::_thesis: verum end; hence latt (L,(.p.>) is C_Lattice ; ::_thesis: verum end; theorem Th84: :: FILTER_2:84 for L being Lattice for p, q being Element of L st L is C_Lattice & L is modular & p [= q holds latt (L,[#p,q#]) is C_Lattice proof let L be Lattice; ::_thesis: for p, q being Element of L st L is C_Lattice & L is modular & p [= q holds latt (L,[#p,q#]) is C_Lattice let p, q be Element of L; ::_thesis: ( L is C_Lattice & L is modular & p [= q implies latt (L,[#p,q#]) is C_Lattice ) assume that A1: L is C_Lattice and A2: L is modular and A3: p [= q ; ::_thesis: latt (L,[#p,q#]) is C_Lattice reconsider K = latt (L,[#p,q#]) as bounded Lattice by A3, Th82; K is complemented proof let b9 be Element of K; :: according to LATTICES:def_19 ::_thesis: ex b1 being Element of the carrier of K st b1 is_a_complement_of b9 reconsider b = b9 as Element of L by Th68; consider a being Element of L such that A4: a is_a_complement_of b by A1, LATTICES:def_19; A5: a "/\" b = Bottom L by A4, LATTICES:def_18; A6: a "\/" b = Top L by A4, LATTICES:def_18; A7: H1(K) = [#p,q#] by Th72; then A8: b [= q by A3, Th62; a "/\" q [= q by LATTICES:6; then ( p [= p "\/" (a "/\" q) & p "\/" (a "/\" q) [= q ) by A3, FILTER_0:6, LATTICES:5; then reconsider a9 = p "\/" (a "/\" q) as Element of K by A3, A7, Th62; take a9 ; ::_thesis: a9 is_a_complement_of b9 A9: p [= b by A3, A7, Th62; thus a9 "\/" b9 = (p "\/" (a "/\" q)) "\/" b by Th73 .= (b "\/" p) "\/" (a "/\" q) by LATTICES:def_5 .= b "\/" (a "/\" q) by A9, LATTICES:def_3 .= (Top L) "/\" q by A2, A6, A8, LATTICES:def_12 .= q by A1 .= Top K by A3, Th82 ; :: according to LATTICES:def_18 ::_thesis: ( b9 "\/" a9 = Top K & a9 "/\" b9 = Bottom K & b9 "/\" a9 = Bottom K ) hence b9 "\/" a9 = Top K ; ::_thesis: ( a9 "/\" b9 = Bottom K & b9 "/\" a9 = Bottom K ) thus a9 "/\" b9 = (p "\/" (a "/\" q)) "/\" b by Th73 .= p "\/" ((a "/\" q) "/\" b) by A2, A9, LATTICES:def_12 .= p "\/" (q "/\" (Bottom L)) by A5, LATTICES:def_7 .= p "\/" (Bottom L) by A1 .= p by A1 .= Bottom K by A3, Th82 ; ::_thesis: b9 "/\" a9 = Bottom K hence b9 "/\" a9 = Bottom K ; ::_thesis: verum end; hence latt (L,[#p,q#]) is C_Lattice ; ::_thesis: verum end; theorem :: FILTER_2:85 for L being Lattice for p, q being Element of L st L is B_Lattice & p [= q holds latt (L,[#p,q#]) is B_Lattice proof let L be Lattice; ::_thesis: for p, q being Element of L st L is B_Lattice & p [= q holds latt (L,[#p,q#]) is B_Lattice let p, q be Element of L; ::_thesis: ( L is B_Lattice & p [= q implies latt (L,[#p,q#]) is B_Lattice ) assume ( L is B_Lattice & p [= q ) ; ::_thesis: latt (L,[#p,q#]) is B_Lattice then latt (L,[#p,q#]) is distributive bounded complemented Lattice by Th77, Th84; hence latt (L,[#p,q#]) is B_Lattice ; ::_thesis: verum end; theorem :: FILTER_2:86 for L being Lattice for S being non empty Subset of L holds ( S is Ideal of L iff for p, q being Element of L holds ( ( p in S & q in S ) iff p "\/" q in S ) ) by Lm1;