let B be B_Lattice; :: thesis: for a being Element of holds B,[:(B /\/ <.a.)),(latt <.a.)):] are_isomorphic
let a be Element of ; :: thesis: B,[:(B /\/ <.a.)),(latt <.a.)):] are_isomorphic
set F = <.a.);
set E = equivalence_wrt <.a.);
deffunc H₃( set ) -> Element of bool the carrier of B = Class (equivalence_wrt <.a.)),$1;
consider g being Function such that
A1: ( dom g = the carrier of B & ( for x being set st x in the carrier of B holds
g . x = H₃(x) ) ) from FUNCT_1:sch 3();
A2: for b being Element of holds (b "\/" (b <=> a)) <=> b = b "\/" a

proof

let b be Element of ; :: thesis: (b "\/" (b <=> a)) <=> b = b "\/" a
A3: (b "\/" (b <=> a)) ` = (b ` ) "/\" ((b <=> a) ` ) by LATTICES:51;
A4: (b ` ) "/\" ((b "/\" (a ` )) "\/" ((b ` ) "/\" a)) = ((b ` ) "/\" (b "/\" (a ` ))) "\/" ((b ` ) "/\" ((b ` ) "/\" a)) by LATTICES:def 11;
A5: (Bottom B) "/\" (a ` ) = Bottom B by LATTICES:40;
A6: b "\/" ((b "/\" a) "\/" ((b ` ) "/\" (a ` ))) = (b "\/" (b "/\" a)) "\/" ((b ` ) "/\" (a ` )) by LATTICES:def 5;
A7: (Bottom B) "\/" ((b ` ) "/\" a) = (b ` ) "/\" a by LATTICES:39;
A8: b <=> a = (b "/\" a) "\/" ((b ` ) "/\" (a ` )) by Th51;
A9: (b ` ) "/\" b = Bottom B by LATTICES:47;
A10: b "/\" b = b by LATTICES:18;
A11: (b ` ) "/\" ((a ` ) "/\" b) = ((b ` ) "/\" (a ` )) "/\" b by LATTICES:def 7;
A12: b "\/" (Bottom B) = b by LATTICES:39;
A13: (b ` ) "/\" (b ` ) = b ` by LATTICES:18;
A14: (b ` ) "/\" ((b ` ) "/\" a) = ((b ` ) "/\" (b ` )) "/\" a by LATTICES:def 7;
A15: (b <=> a) ` = (b "/\" (a ` )) "\/" ((b ` ) "/\" a) by Th52;
A16: (b ` ) "/\" (b "/\" (a ` )) = ((b ` ) "/\" b) "/\" (a ` ) by LATTICES:def 7;
A17: (b "\/" ((b ` ) "/\" (a ` ))) "/\" b = (b "/\" b) "\/" (((b ` ) "/\" (a ` )) "/\" b) by LATTICES:def 11;
A18: (b "/\" a) "\/" b = b by LATTICES:def 8;
(b "\/" (b <=> a)) <=> b = ((b "\/" (b <=> a)) "/\" b) "\/" (((b "\/" (b <=> a)) ` ) "/\" (b ` )) by Th51;
hence (b "\/" (b <=> a)) <=> b = b "\/" ((b "/\" a) "\/" ((b ` ) "/\" a)) by A3, A15, A4, A16, A9, A14, A13, A5, A7, A8, A6, A18, A17, A11, A10, A12, LATTICES:def 5
.= b "\/" ((b "\/" (b ` )) "/\" a) by LATTICES:def 11
.= b "\/" ((Top B) "/\" a) by LATTICES:48
.= b "\/" a by LATTICES:43 ;
:: thesis: verum

end;

set S = LattRel [:(B /\/ <.a.)),(latt <.a.)):];
A19: field (LattRel [:(B /\/ <.a.)),(latt <.a.)):]) = the carrier of [:(B /\/ <.a.)),(latt <.a.)):] by Th33;
A20: B is I_Lattice by FILTER_0:40;
then reconsider o1 = H₁(B), o2 = H₂(B) as BinOp of equivalence_wrt <.a.) by Th13, Th14;
A21: LattStr(# (Class (equivalence_wrt <.a.))),(o1 /\/ (equivalence_wrt <.a.))),(o2 /\/ (equivalence_wrt <.a.))) #) = B /\/ <.a.) by A20, Def5;
set R = LattRel B;
deffunc H₄( Element of ) -> Element of the carrier of B = ($1 "\/" ($1 <=> a)) <=> $1;
consider h being UnOp of the carrier of B such that
A22: for b being Element of holds h . b = H₄(b) from FUNCT_2:sch 4();
take f = <:g,h:>; :: according to WELLORD1:def 8,FILTER_1:def 9 :: thesis: f is_isomorphism_of LattRel B, LattRel [:(B /\/ <.a.)),(latt <.a.)):]
A23: field (LattRel B) = the carrier of B by Th33;
A24: dom h = dom g by A1, FUNCT_2:def 1;
hence A25: dom f = field (LattRel B) by A1, A23, FUNCT_3:70; :: according to WELLORD1:def 7 :: thesis: ( rng f = field (LattRel [:(B /\/ <.a.)),(latt <.a.)):]) & f is one-to-one & ( for b₁, b₂ being set holds
( ( not [b₁,b₂] in LattRel B or ( b₁ in field (LattRel B) & b₂ in field (LattRel B) & [(f . b₁),(f . b₂)] in LattRel [:(B /\/ <.a.)),(latt <.a.)):] ) ) & ( not b₁ in field (LattRel B) or not b₂ in field (LattRel B) or not [(f . b₁),(f . b₂)] in LattRel [:(B /\/ <.a.)),(latt <.a.)):] or [b₁,b₂] in LattRel B ) ) ) )
A26: for b being Element of holds h . b is Element of

proof

let b be Element of ; :: thesis: h . b is Element of
b "\/" (b <=> a) in Class (equivalence_wrt <.a.)),b by Th61;
then [(b "\/" (b <=> a)),b] in equivalence_wrt <.a.) by EQREL_1:27;
then A27: (b "\/" (b <=> a)) <=> b in <.a.) by FILTER_0:def 12;
h . b = (b "\/" (b <=> a)) <=> b by A22;
hence h . b is Element of by A27, FILTER_0:63; :: thesis: verum

end;

thus rng f c= field (LattRel [:(B /\/ <.a.)),(latt <.a.)):]) :: according to XBOOLE_0:def 10 :: thesis: ( field (LattRel [:(B /\/ <.a.)),(latt <.a.)):]) c= rng f & f is one-to-one & ( for b₁, b₂ being set holds
( ( not [b₁,b₂] in LattRel B or ( b₁ in field (LattRel B) & b₂ in field (LattRel B) & [(f . b₁),(f . b₂)] in LattRel [:(B /\/ <.a.)),(latt <.a.)):] ) ) & ( not b₁ in field (LattRel B) or not b₂ in field (LattRel B) or not [(f . b₁),(f . b₂)] in LattRel [:(B /\/ <.a.)),(latt <.a.)):] or [b₁,b₂] in LattRel B ) ) ) )

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in field (LattRel [:(B /\/ <.a.)),(latt <.a.)):]) )
assume x in rng f ; :: thesis: x in field (LattRel [:(B /\/ <.a.)),(latt <.a.)):])
then consider y being set such that
A28: y in dom f and
A29: x = f . y by FUNCT_1:def 5;
reconsider y = y as Element of by A1, A24, A28, FUNCT_3:70;
reconsider z2 = h . y as Element of by A26;
g . y = EqClass (equivalence_wrt <.a.)),y by A1;
then reconsider z1 = g . y as Element of by A21;
x = [z1,z2] by A28, A29, FUNCT_3:def 8;
hence x in field (LattRel [:(B /\/ <.a.)),(latt <.a.)):]) by A19; :: thesis: verum

end;

A30: the carrier of (latt <.a.)) = <.a.) by FILTER_0:63;
thus field (LattRel [:(B /\/ <.a.)),(latt <.a.)):]) c= rng f :: thesis: ( f is one-to-one & ( for b₁, b₂ being set holds
( ( not [b₁,b₂] in LattRel B or ( b₁ in field (LattRel B) & b₂ in field (LattRel B) & [(f . b₁),(f . b₂)] in LattRel [:(B /\/ <.a.)),(latt <.a.)):] ) ) & ( not b₁ in field (LattRel B) or not b₂ in field (LattRel B) or not [(f . b₁),(f . b₂)] in LattRel [:(B /\/ <.a.)),(latt <.a.)):] or [b₁,b₂] in LattRel B ) ) ) )

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in field (LattRel [:(B /\/ <.a.)),(latt <.a.)):]) or x in rng f )
assume x in field (LattRel [:(B /\/ <.a.)),(latt <.a.)):]) ; :: thesis: x in rng f
then consider y being Element of Class (equivalence_wrt <.a.)), z being Element of <.a.) such that
A31: x = [y,z] by A19, A30, A21, DOMAIN_1:9;
consider b being Element of such that
A32: y = Class (equivalence_wrt <.a.)),b by EQREL_1:45;
set ty = b "\/" (b <=> a);
(b "\/" (b <=> a)) <=> ((b "\/" (b <=> a)) <=> z) = z by Th54;
then ((b "\/" (b <=> a)) <=> z) <=> (b "\/" (b <=> a)) = z ;
then A33: [((b "\/" (b <=> a)) <=> z),(b "\/" (b <=> a))] in equivalence_wrt <.a.) by FILTER_0:def 12;
b "\/" (b <=> a) in y by A32, Th61;
then y = Class (equivalence_wrt <.a.)),(b "\/" (b <=> a)) by A32, EQREL_1:31;
then A34: (b "\/" (b <=> a)) <=> z in y by A33, EQREL_1:27;
then A35: y = Class (equivalence_wrt <.a.)),((b "\/" (b <=> a)) <=> z) by A32, EQREL_1:31;
then A36: b "\/" (b <=> a) [= ((b "\/" (b <=> a)) <=> z) "\/" (((b "\/" (b <=> a)) <=> z) <=> a) by A32, Th61;
y = Class (equivalence_wrt <.a.)),((b "\/" (b <=> a)) <=> z) by A32, A34, EQREL_1:31;
then A37: g . ((b "\/" (b <=> a)) <=> z) = y by A1;
((b "\/" (b <=> a)) <=> z) "\/" (((b "\/" (b <=> a)) <=> z) <=> a) [= b "\/" (b <=> a) by A32, A35, Th61;
then A38: ((b "\/" (b <=> a)) <=> z) "\/" (((b "\/" (b <=> a)) <=> z) <=> a) = b "\/" (b <=> a) by A36, LATTICES:26;
h . ((b "\/" (b <=> a)) <=> z) = (((b "\/" (b <=> a)) <=> z) "\/" (((b "\/" (b <=> a)) <=> z) <=> a)) <=> ((b "\/" (b <=> a)) <=> z) by A22;
then h . ((b "\/" (b <=> a)) <=> z) = z by A38, Th54;
then x = f . ((b "\/" (b <=> a)) <=> z) by A23, A25, A31, A37, FUNCT_3:def 8;
hence x in rng f by A23, A25, FUNCT_1:def 5; :: thesis: verum

end;

thus f is one-to-one :: thesis: for b₁, b₂ being set holds
( ( not [b₁,b₂] in LattRel B or ( b₁ in field (LattRel B) & b₂ in field (LattRel B) & [(f . b₁),(f . b₂)] in LattRel [:(B /\/ <.a.)),(latt <.a.)):] ) ) & ( not b₁ in field (LattRel B) or not b₂ in field (LattRel B) or not [(f . b₁),(f . b₂)] in LattRel [:(B /\/ <.a.)),(latt <.a.)):] or [b₁,b₂] in LattRel B ) )

proof

let x be set ; :: according to FUNCT_1:def 8 :: thesis: for b₁ being set holds
( not x in dom f or not b₁ in dom f or not f . x = f . b₁ or x = b₁ )
let y be set ; :: thesis: ( not x in dom f or not y in dom f or not f . x = f . y or x = y )
assume that
A39: x in dom f and
A40: y in dom f ; :: thesis: ( not f . x = f . y or x = y )
reconsider x' = x, y' = y as Element of by A1, A24, A39, A40, FUNCT_3:70;
assume A41: f . x = f . y ; :: thesis: x = y
A42: g . y' = Class (equivalence_wrt <.a.)),y' by A1;
A43: h . y' = (y' "\/" (y' <=> a)) <=> y' by A22;
A44: h . x' = (x' "\/" (x' <=> a)) <=> x' by A22;
A45: g . x' = Class (equivalence_wrt <.a.)),x' by A1;
A46: f . y = [(g . y'),(h . y')] by A23, A25, FUNCT_3:def 8;
A47: f . x = [(g . x'),(h . x')] by A23, A25, FUNCT_3:def 8;
then A48: g . x = g . y by A46, A41, ZFMISC_1:33;
then A49: y' "\/" (y' <=> a) [= x' "\/" (x' <=> a) by A45, A42, Th61;
x' "\/" (x' <=> a) [= y' "\/" (y' <=> a) by A45, A42, A48, Th61;
then A50: y' "\/" (y' <=> a) = x' "\/" (x' <=> a) by A49, LATTICES:26;
h . x = h . y by A47, A46, A41, ZFMISC_1:33;
hence x = y by A44, A43, A50, Th53; :: thesis: verum

end;

let x, y be set ; :: thesis: ( ( not [x,y] in LattRel B or ( x in field (LattRel B) & y in field (LattRel B) & [(f . x),(f . y)] in LattRel [:(B /\/ <.a.)),(latt <.a.)):] ) ) & ( not x in field (LattRel B) or not y in field (LattRel B) or not [(f . x),(f . y)] in LattRel [:(B /\/ <.a.)),(latt <.a.)):] or [x,y] in LattRel B ) )
A51: the carrier of (latt <.a.)) = <.a.) by FILTER_0:63;
thus ( [x,y] in LattRel B implies ( x in field (LattRel B) & y in field (LattRel B) & [(f . x),(f . y)] in LattRel [:(B /\/ <.a.)),(latt <.a.)):] ) ) :: thesis: ( not x in field (LattRel B) or not y in field (LattRel B) or not [(f . x),(f . y)] in LattRel [:(B /\/ <.a.)),(latt <.a.)):] or [x,y] in LattRel B )

proof

assume A52: [x,y] in LattRel B ; :: thesis: ( x in field (LattRel B) & y in field (LattRel B) & [(f . x),(f . y)] in LattRel [:(B /\/ <.a.)),(latt <.a.)):] )
then reconsider x' = x, y' = y as Element of by A23, RELAT_1:30;
A53: x' [= y' by A52, Th32;
thus ( x in field (LattRel B) & y in field (LattRel B) ) by A52, RELAT_1:30; :: thesis: [(f . x),(f . y)] in LattRel [:(B /\/ <.a.)),(latt <.a.)):]
A54: Top B in <.a.) by FILTER_0:12;
x' "/\" (Top B) = x' by LATTICES:43;
then Top B [= x' => y' by A20, A53, FILTER_0:def 8;
then x' => y' in <.a.) by A54, FILTER_0:9;
then A55: x' /\/ <.a.) [= y' /\/ <.a.) by A20, Th16;
A56: h . x' = (x' "\/" (x' <=> a)) <=> x' by A22;
A57: y' "\/" (y' <=> a) in Class (equivalence_wrt <.a.)),y' by Th61;
A58: (y' "\/" (y' <=> a)) <=> y' = y' "\/" a by A2;
A59: (x' "\/" (x' <=> a)) <=> x' = x' "\/" a by A2;
A60: h . y' = (y' "\/" (y' <=> a)) <=> y' by A22;
x' "\/" (x' <=> a) in Class (equivalence_wrt <.a.)),x' by Th61;
then reconsider hx = h . x, hy = h . y as Element of by A20, A51, A56, A60, A57, Lm4;
A61: Class (equivalence_wrt <.a.)),x' = g . x' by A1;
x' "\/" a [= y' "\/" a by A53, FILTER_0:1;
then hx [= hy by A56, A60, A59, A58, FILTER_0:65;
then A62: [(x' /\/ <.a.)),hx] [= [(y' /\/ <.a.)),hy] by A55, Th37;
A63: y' /\/ <.a.) = Class (equivalence_wrt <.a.)),y' by A20, Def6;
A64: Class (equivalence_wrt <.a.)),y' = g . y' by A1;
A65: f . y' = [(g . y'),(h . y')] by A23, A25, FUNCT_3:def 8;
A66: f . x' = [(g . x'),(h . x')] by A23, A25, FUNCT_3:def 8;
x' /\/ <.a.) = Class (equivalence_wrt <.a.)),x' by A20, Def6;
hence [(f . x),(f . y)] in LattRel [:(B /\/ <.a.)),(latt <.a.)):] by A61, A63, A64, A66, A65, A62; :: thesis: verum

end;

assume that
A67: x in field (LattRel B) and
A68: y in field (LattRel B) ; :: thesis: ( not [(f . x),(f . y)] in LattRel [:(B /\/ <.a.)),(latt <.a.)):] or [x,y] in LattRel B )
reconsider x' = x, y' = y as Element of by A67, A68, Th33;
A69: h . x' = (x' "\/" (x' <=> a)) <=> x' by A22;
A70: f . y' = [(g . y'),(h . y')] by A23, A25, FUNCT_3:def 8;
A71: y' /\/ <.a.) = Class (equivalence_wrt <.a.)),y' by A20, Def6;
A72: Class (equivalence_wrt <.a.)),x' = g . x' by A1;
A73: (y' "\/" (y' <=> a)) <=> y' = y' "\/" a by A2;
A74: (x' "\/" (x' <=> a)) <=> x' = x' "\/" a by A2;
A75: y' "/\" x' [= y' by LATTICES:23;
A76: y' "\/" (y' <=> a) in Class (equivalence_wrt <.a.)),y' by Th61;
A77: h . y' = (y' "\/" (y' <=> a)) <=> y' by A22;
x' "\/" (x' <=> a) in Class (equivalence_wrt <.a.)),x' by Th61;
then reconsider hx = h . x, hy = h . y as Element of by A20, A51, A69, A77, A76, Lm4;
assume A78: [(f . x),(f . y)] in LattRel [:(B /\/ <.a.)),(latt <.a.)):] ; :: thesis: [x,y] in LattRel B
A79: f . x' = [(g . x'),(h . x')] by A23, A25, FUNCT_3:def 8;
A80: Class (equivalence_wrt <.a.)),y' = g . y' by A1;
x' /\/ <.a.) = Class (equivalence_wrt <.a.)),x' by A20, Def6;
then A81: [(x' /\/ <.a.)),hx] [= [(y' /\/ <.a.)),hy] by A71, A72, A80, A79, A70, A78, Th32;
then x' /\/ <.a.) [= y' /\/ <.a.) by Th37;
then A82: x' => y' in <.a.) by A20, Th16;
x' => y' = (x' ` ) "\/" y' by FILTER_0:55;
then a [= (x' ` ) "\/" y' by A82, FILTER_0:18;
then A83: x' "/\" a [= x' "/\" ((x' ` ) "\/" y') by LATTICES:27;
A84: (Bottom B) "\/" (x' "/\" y') = x' "/\" y' by LATTICES:39;
hx [= hy by A81, Th37;
then x' "\/" a [= y' "\/" a by A69, A77, A74, A73, FILTER_0:65;
then A85: x' "/\" (x' "\/" a) [= x' "/\" (y' "\/" a) by LATTICES:27;
A86: x' "/\" (x' ` ) = Bottom B by LATTICES:47;
x' "/\" ((x' ` ) "\/" y') = (x' "/\" (x' ` )) "\/" (x' "/\" y') by LATTICES:def 11;
then x' "/\" a [= y' by A83, A86, A84, A75, LATTICES:25;
then A87: (x' "/\" y') "\/" (x' "/\" a) [= y' by A75, FILTER_0:6;
x' [= x' "\/" a by LATTICES:22;
then x' "/\" (x' "\/" a) = x' by LATTICES:21;
then x' [= (x' "/\" y') "\/" (x' "/\" a) by A85, LATTICES:def 11;
then x' [= y' by A87, LATTICES:25;
hence [x,y] in LattRel B ; :: thesis: verum