let B be B_Lattice; :: thesis: for c, d being Element of B holds
( c "\/" (c <=> d) in Class ((equivalence_wrt <.d.)),c) & ( for b being Element of B st b in Class ((equivalence_wrt <.d.)),c) holds
b [= c "\/" (c <=> d) ) )
let c, d be Element of B; :: thesis: ( c "\/" (c <=> d) in Class ((equivalence_wrt <.d.)),c) & ( for b being Element of B st b in Class ((equivalence_wrt <.d.)),c) holds
b [= c "\/" (c <=> d) ) )
set A = Class ((equivalence_wrt <.d.)),c);
A2: c in Class ((equivalence_wrt <.d.)),c) by EQREL_1:28;
A3: (c <=> d) <=> c = c <=> (c <=> d) ;
A4: d in <.d.) ;
c <=> (c <=> d) = d by Th54;
then c <=> d in Class ((equivalence_wrt <.d.)),c) by A4, A3, Lm4;
hence c "\/" (c <=> d) in Class ((equivalence_wrt <.d.)),c) by A2, Th60; :: thesis: for b being Element of B st b in Class ((equivalence_wrt <.d.)),c) holds
b [= c "\/" (c <=> d)
let b be Element of B; :: thesis: ( b in Class ((equivalence_wrt <.d.)),c) implies b [= c "\/" (c <=> d) )
assume b in Class ((equivalence_wrt <.d.)),c) ; :: thesis: b [= c "\/" (c <=> d)
then b <=> c in <.d.) by Lm4;
then A5: d [= b <=> c by FILTER_0:18;
(b <=> c) ` = (b "/\" (c `)) "\/" ((b `) "/\" c) by Th52;
then (b "/\" (c `)) "\/" ((b `) "/\" c) [= d ` by A5, LATTICES:53;
then A6: ((b "/\" (c `)) "\/" ((b `) "/\" c)) "/\" (c `) [= (d `) "/\" (c `) by LATTICES:27;
A7: ((b "/\" (c `)) "\/" ((b `) "/\" c)) "/\" (c `) = ((b "/\" (c `)) "/\" (c `)) "\/" (((b `) "/\" c) "/\" (c `)) by LATTICES:def 11;
A8: ((b `) "/\" c) "/\" (c `) = (b `) "/\" (c "/\" (c `)) by LATTICES:def 7;
A9: (b "/\" (c `)) "\/" (Bottom B) = b "/\" (c `) by LATTICES:39;
A10: ((c `) "/\" (d `)) "\/" (b "/\" c) [= ((c `) "/\" (d `)) "\/" c by FILTER_0:1, LATTICES:23;
A11: b "/\" (Top B) = b by LATTICES:43;
A12: (b "/\" (c `)) "\/" (b "/\" c) = b "/\" ((c `) "\/" c) by LATTICES:def 11;
A13: (b `) "/\" (Bottom B) = Bottom B by LATTICES:40;
A14: (c "\/" (c "/\" d)) "\/" ((c `) "/\" (d `)) = c "\/" ((c "/\" d) "\/" ((c `) "/\" (d `))) by LATTICES:def 5;
A15: c = c "\/" (c "/\" d) by LATTICES:def 8;
A16: (c "/\" d) "\/" ((c `) "/\" (d `)) = c <=> d by Th51;
A17: c ` = (c `) "/\" (c `) by LATTICES:18;
A18: (c `) "\/" c = Top B by LATTICES:48;
A19: Bottom B = c "/\" (c `) by LATTICES:47;
(b "/\" (c `)) "/\" (c `) = b "/\" ((c `) "/\" (c `)) by LATTICES:def 7;
then (b "/\" (c `)) "\/" (b "/\" c) [= ((c `) "/\" (d `)) "\/" (b "/\" c) by A6, A17, A7, A9, A8, A19, A13, FILTER_0:1;
hence b [= c "\/" (c <=> d) by A12, A18, A11, A10, A15, A16, A14, LATTICES:25; :: thesis: verum