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: B is I_Lattice by FILTER_0:40;
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 A1, A4, A3, Lm4;
hence c "\/" (c <=> d) in Class (equivalence_wrt <.d.)),c by A1, 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 A1, 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