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);
A1: c in Class ((equivalence_wrt <.d.)),c) by EQREL_1:20;
A2: (c <=> d) <=> c = c <=> (c <=> d) ;
A3: d in <.d.) ;
c <=> (c <=> d) = d by Th54;
then c <=> d in Class ((equivalence_wrt <.d.)),c) by A3, A2, Lm4;
hence c "\/" (c <=> d) in Class ((equivalence_wrt <.d.)),c) by A1, 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 A4: d [= b <=> c by FILTER_0:15;
(b <=> c) ` = (b "/\" (c `)) "\/" ((b `) "/\" c) by Th52;
then (b "/\" (c `)) "\/" ((b `) "/\" c) [= d ` by A4, LATTICES:26;
then A5: ((b "/\" (c `)) "\/" ((b `) "/\" c)) "/\" (c `) [= (d `) "/\" (c `) by LATTICES:9;
A6: ((b "/\" (c `)) "\/" ((b `) "/\" c)) "/\" (c `) = ((b "/\" (c `)) "/\" (c `)) "\/" (((b `) "/\" c) "/\" (c `)) by LATTICES:def 11;
A7: ((b `) "/\" c) "/\" (c `) = (b `) "/\" (c "/\" (c `)) by LATTICES:def 7;
A8: (b "/\" (c `)) "\/" (Bottom B) = b "/\" (c `) by LATTICES:14;
A9: ((c `) "/\" (d `)) "\/" (b "/\" c) [= ((c `) "/\" (d `)) "\/" c by FILTER_0:1, LATTICES:6;
A10: b "/\" (Top B) = b by LATTICES:17;
A11: (b "/\" (c `)) "\/" (b "/\" c) = b "/\" ((c `) "\/" c) by LATTICES:def 11;
A12: (b `) "/\" (Bottom B) = Bottom B by LATTICES:15;
A13: (c "\/" (c "/\" d)) "\/" ((c `) "/\" (d `)) = c "\/" ((c "/\" d) "\/" ((c `) "/\" (d `))) by LATTICES:def 5;
A14: c = c "\/" (c "/\" d) by LATTICES:def 8;
A15: (c "/\" d) "\/" ((c `) "/\" (d `)) = c <=> d by Th51;
A16: c ` = (c `) "/\" (c `) by LATTICES:2;
A17: (c `) "\/" c = Top B by LATTICES:21;
A18: Bottom B = c "/\" (c `) by LATTICES:20;
(b "/\" (c `)) "/\" (c `) = b "/\" ((c `) "/\" (c `)) by LATTICES:def 7;
then (b "/\" (c `)) "\/" (b "/\" c) [= ((c `) "/\" (d `)) "\/" (b "/\" c) by A5, A16, A6, A8, A7, A18, A12, FILTER_0:1;
hence b [= c "\/" (c <=> d) by A11, A17, A10, A9, A14, A15, A13, LATTICES:7; :: thesis: verum