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 Th53;

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, Th59; :: 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 Th51;

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: ((c `) "/\" (d `)) "\/" (b "/\" c) [= ((c `) "/\" (d `)) "\/" c by FILTER_0:1, LATTICES:6;

A9: (b "/\" (c `)) "\/" (b "/\" c) = b "/\" ((c `) "\/" c) by LATTICES:def 11;

A10: (c "\/" (c "/\" d)) "\/" ((c `) "/\" (d `)) = c "\/" ((c "/\" d) "\/" ((c `) "/\" (d `))) by LATTICES:def 5;

A11: c = c "\/" (c "/\" d) by LATTICES:def 8;

A12: (c "/\" d) "\/" ((c `) "/\" (d `)) = c <=> d by Th50;

A13: (c `) "\/" c = Top B by LATTICES:21;

A14: 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, A6, A7, A14, FILTER_0:1;

hence b [= c "\/" (c <=> d) by A9, A13, A8, A11, A12, A10, LATTICES:7; :: thesis: verum

( 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 Th53;

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, Th59; :: 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 Th51;

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: ((c `) "/\" (d `)) "\/" (b "/\" c) [= ((c `) "/\" (d `)) "\/" c by FILTER_0:1, LATTICES:6;

A9: (b "/\" (c `)) "\/" (b "/\" c) = b "/\" ((c `) "\/" c) by LATTICES:def 11;

A10: (c "\/" (c "/\" d)) "\/" ((c `) "/\" (d `)) = c "\/" ((c "/\" d) "\/" ((c `) "/\" (d `))) by LATTICES:def 5;

A11: c = c "\/" (c "/\" d) by LATTICES:def 8;

A12: (c "/\" d) "\/" ((c `) "/\" (d `)) = c <=> d by Th50;

A13: (c `) "\/" c = Top B by LATTICES:21;

A14: 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, A6, A7, A14, FILTER_0:1;

hence b [= c "\/" (c <=> d) by A9, A13, A8, A11, A12, A10, LATTICES:7; :: thesis: verum