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;
( d in <.d.) & c <=> (c <=> d) = d & (c <=> d) <=> c = c <=> (c <=> d) ) by Th54;
then ( c <=> d in Class (equivalence_wrt <.d.)),c & c in Class (equivalence_wrt <.d.)),c ) by A1, Lm4, EQREL_1:28;
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 A1, Lm4;
then ( d [= b <=> c & (b <=> c) ` = (b "/\" (c ` )) "\/" ((b ` ) "/\" c) ) by Th52, FILTER_0:18;
then (b "/\" (c ` )) "\/" ((b ` ) "/\" c) [= d ` by LATTICES:53;
then ( ((b "/\" (c ` )) "\/" ((b ` ) "/\" c)) "/\" (c ` ) [= (d ` ) "/\" (c ` ) & (b "/\" (c ` )) "/\" (c ` ) = b "/\" ((c ` ) "/\" (c ` )) & c ` = (c ` ) "/\" (c ` ) & ((b "/\" (c ` )) "\/" ((b ` ) "/\" c)) "/\" (c ` ) = ((b "/\" (c ` )) "/\" (c ` )) "\/" (((b ` ) "/\" c) "/\" (c ` )) & (b "/\" (c ` )) "\/" (Bottom B) = b "/\" (c ` ) & ((b ` ) "/\" c) "/\" (c ` ) = (b ` ) "/\" (c "/\" (c ` )) & Bottom B = c "/\" (c ` ) & (d ` ) "/\" (c ` ) = (c ` ) "/\" (d ` ) & c "/\" b [= c & c "/\" b = b "/\" c & c "/\" d [= c & (c "/\" d) "\/" c = c "\/" (c "/\" d) & (b ` ) "/\" (Bottom B) = Bottom B ) by LATTICES:18, LATTICES:23, LATTICES:27, LATTICES:39, LATTICES:40, LATTICES:47, LATTICES:def 7, LATTICES:def 11;
then ( (b "/\" (c ` )) "\/" (b "/\" c) [= ((c ` ) "/\" (d ` )) "\/" (b "/\" c) & (b "/\" (c ` )) "\/" (b "/\" c) = b "/\" ((c ` ) "\/" c) & (c ` ) "\/" c = Top B & b "/\" (Top B) = b & ((c ` ) "/\" (d ` )) "\/" (b "/\" c) [= ((c ` ) "/\" (d ` )) "\/" c & ((c ` ) "/\" (d ` )) "\/" c = c "\/" ((c ` ) "/\" (d ` )) & c = c "\/" (c "/\" d) & (c "/\" d) "\/" ((c ` ) "/\" (d ` )) = c <=> d & (c "\/" (c "/\" d)) "\/" ((c ` ) "/\" (d ` )) = c "\/" ((c "/\" d) "\/" ((c ` ) "/\" (d ` ))) ) by Th51, FILTER_0:1, LATTICES:43, LATTICES:48, LATTICES:def 5, LATTICES:def 8, LATTICES:def 11;
hence b [= c "\/" (c <=> d) by LATTICES:25; :: thesis: verum