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