let B be B_Lattice; :: thesis: for a, b, c being Element of B st a <=> b = a <=> c holds
b = c
let a, b, c be Element of B; :: thesis: ( a <=> b = a <=> c implies b = c )
set ab = a "/\" b;
set ac = a "/\" c;
set bc = b "/\" c;
set b'c' = (b ` ) "/\" (c ` );
set a'b' = (a ` ) "/\" (b ` );
set a'c' = (a ` ) "/\" (c ` );
set a'b = (a ` ) "/\" b;
set a'c = (a ` ) "/\" c;
set ab' = a "/\" (b ` );
set ac' = a "/\" (c ` );
A1: ( (a <=> b) <=> (a <=> c) = ((a <=> b) "/\" (a <=> c)) "\/" (((a <=> b) ` ) "/\" ((a <=> c) ` )) & a <=> b = (a "/\" b) "\/" ((a ` ) "/\" (b ` )) & a <=> c = (a "/\" c) "\/" ((a ` ) "/\" (c ` )) & (a <=> b) ` = (a "/\" (b ` )) "\/" ((a ` ) "/\" b) & (a <=> c) ` = (a "/\" (c ` )) "\/" ((a ` ) "/\" c) & ((a "/\" b) "\/" ((a ` ) "/\" (b ` ))) "/\" ((a "/\" c) "\/" ((a ` ) "/\" (c ` ))) = ((a "/\" b) "/\" ((a "/\" c) "\/" ((a ` ) "/\" (c ` )))) "\/" (((a ` ) "/\" (b ` )) "/\" ((a "/\" c) "\/" ((a ` ) "/\" (c ` )))) & (a "/\" b) "/\" ((a "/\" c) "\/" ((a ` ) "/\" (c ` ))) = ((a "/\" b) "/\" (a "/\" c)) "\/" ((a "/\" b) "/\" ((a ` ) "/\" (c ` ))) & (a "/\" b) "/\" ((a ` ) "/\" (c ` )) = ((a "/\" b) "/\" (a ` )) "/\" (c ` ) & ((a ` ) "/\" (b ` )) "/\" ((a "/\" c) "\/" ((a ` ) "/\" (c ` ))) = (((a ` ) "/\" (b ` )) "/\" (a "/\" c)) "\/" (((a ` ) "/\" (b ` )) "/\" ((a ` ) "/\" (c ` ))) & (b "/\" a) "/\" (a ` ) = b "/\" (a "/\" (a ` )) & b "/\" (Bottom B) = Bottom B & (b ` ) "/\" (Bottom B) = Bottom B & (Bottom B) "/\" c = Bottom B & (Bottom B) "/\" (c ` ) = Bottom B & a "/\" (a ` ) = Bottom B & (a ` ) "/\" a = Bottom B & a "/\" b = b "/\" a & (a ` ) "/\" (b ` ) = (b ` ) "/\" (a ` ) & ((a ` ) "/\" (b ` )) "/\" (a "/\" c) = (((a ` ) "/\" (b ` )) "/\" a) "/\" c & ((b ` ) "/\" (a ` )) "/\" a = (b ` ) "/\" ((a ` ) "/\" a) & ((a "/\" b) "/\" (a "/\" c)) "\/" (Bottom B) = (a "/\" b) "/\" (a "/\" c) & (Bottom B) "\/" (((a ` ) "/\" (b ` )) "/\" ((a ` ) "/\" (c ` ))) = ((a ` ) "/\" (b ` )) "/\" ((a ` ) "/\" (c ` )) & ((a "/\" (b ` )) "\/" ((a ` ) "/\" b)) "/\" ((a "/\" (c ` )) "\/" ((a ` ) "/\" c)) = ((a "/\" (b ` )) "/\" ((a "/\" (c ` )) "\/" ((a ` ) "/\" c))) "\/" (((a ` ) "/\" b) "/\" ((a "/\" (c ` )) "\/" ((a ` ) "/\" c))) & (a "/\" (b ` )) "/\" ((a "/\" (c ` )) "\/" ((a ` ) "/\" c)) = ((a "/\" (b ` )) "/\" (a "/\" (c ` ))) "\/" ((a "/\" (b ` )) "/\" ((a ` ) "/\" c)) & (a "/\" (b ` )) "/\" ((a ` ) "/\" c) = ((a "/\" (b ` )) "/\" (a ` )) "/\" c & ((a ` ) "/\" b) "/\" ((a "/\" (c ` )) "\/" ((a ` ) "/\" c)) = (((a ` ) "/\" b) "/\" (a "/\" (c ` ))) "\/" (((a ` ) "/\" b) "/\" ((a ` ) "/\" c)) & ((b ` ) "/\" a) "/\" (a ` ) = (b ` ) "/\" (a "/\" (a ` )) & (b ` ) "/\" (Bottom B) = Bottom B & b "/\" (Bottom B) = Bottom B & (Bottom B) "/\" (c ` ) = Bottom B & (Bottom B) "/\" c = Bottom B & a "/\" (a ` ) = Bottom B & (a ` ) "/\" a = Bottom B & a "/\" (b ` ) = (b ` ) "/\" a & (a ` ) "/\" b = b "/\" (a ` ) & ((a ` ) "/\" b) "/\" (a "/\" (c ` )) = (((a ` ) "/\" b) "/\" a) "/\" (c ` ) & (b "/\" (a ` )) "/\" a = b "/\" ((a ` ) "/\" a) & ((a "/\" (b ` )) "/\" (a "/\" (c ` ))) "\/" (Bottom B) = (a "/\" (b ` )) "/\" (a "/\" (c ` )) & (Bottom B) "\/" (((a ` ) "/\" b) "/\" ((a ` ) "/\" c)) = ((a ` ) "/\" b) "/\" ((a ` ) "/\" c) ) by Th51, Th52, LATTICES:39, LATTICES:40, LATTICES:47, LATTICES:def 7, LATTICES:def 11;
( (a "/\" b) "/\" (a "/\" c) = ((a "/\" b) "/\" a) "/\" c & (a "/\" b) "/\" a = a "/\" (a "/\" b) & a "/\" (a "/\" b) = (a "/\" a) "/\" b & a "/\" a = a & ((a ` ) "/\" (b ` )) "/\" ((a ` ) "/\" (c ` )) = (((a ` ) "/\" (b ` )) "/\" (a ` )) "/\" (c ` ) & ((a ` ) "/\" (b ` )) "/\" (a ` ) = (a ` ) "/\" ((a ` ) "/\" (b ` )) & (a ` ) "/\" ((a ` ) "/\" (b ` )) = ((a ` ) "/\" (a ` )) "/\" (b ` ) & (a ` ) "/\" (a ` ) = a ` & (a "/\" (b ` )) "/\" (a "/\" (c ` )) = ((a "/\" (b ` )) "/\" a) "/\" (c ` ) & (a "/\" (b ` )) "/\" a = a "/\" (a "/\" (b ` )) & (a "/\" b) "/\" c = a "/\" (b "/\" c) & a "/\" (a "/\" (b ` )) = (a "/\" a) "/\" (b ` ) & ((a ` ) "/\" b) "/\" ((a ` ) "/\" c) = (((a ` ) "/\" b) "/\" (a ` )) "/\" c & ((a ` ) "/\" b) "/\" (a ` ) = (a ` ) "/\" ((a ` ) "/\" b) & ((a ` ) "/\" b) "/\" c = (a ` ) "/\" (b "/\" c) & (a "/\" (b ` )) "/\" (c ` ) = a "/\" ((b ` ) "/\" (c ` )) & ((a ` ) "/\" (b ` )) "/\" (c ` ) = (a ` ) "/\" ((b ` ) "/\" (c ` )) & (a ` ) "/\" ((a ` ) "/\" b) = ((a ` ) "/\" (a ` )) "/\" b & ((a "/\" (b "/\" c)) "\/" ((a ` ) "/\" ((b ` ) "/\" (c ` )))) "\/" ((a "/\" ((b ` ) "/\" (c ` ))) "\/" ((a ` ) "/\" (b "/\" c))) = (((a "/\" (b "/\" c)) "\/" ((a ` ) "/\" ((b ` ) "/\" (c ` )))) "\/" (a "/\" ((b ` ) "/\" (c ` )))) "\/" ((a ` ) "/\" (b "/\" c)) & ((a "/\" (b "/\" c)) "\/" ((a ` ) "/\" ((b ` ) "/\" (c ` )))) "\/" (a "/\" ((b ` ) "/\" (c ` ))) = (a "/\" ((b ` ) "/\" (c ` ))) "\/" ((a "/\" (b "/\" c)) "\/" ((a ` ) "/\" ((b ` ) "/\" (c ` )))) & (a "/\" ((b ` ) "/\" (c ` ))) "\/" ((a "/\" (b "/\" c)) "\/" ((a ` ) "/\" ((b ` ) "/\" (c ` )))) = ((a "/\" ((b ` ) "/\" (c ` ))) "\/" (a "/\" (b "/\" c))) "\/" ((a ` ) "/\" ((b ` ) "/\" (c ` ))) & (a "/\" ((b ` ) "/\" (c ` ))) "\/" (a "/\" (b "/\" c)) = a "/\" (((b ` ) "/\" (c ` )) "\/" (b "/\" c)) & ((b ` ) "/\" (c ` )) "\/" (b "/\" c) = (b "/\" c) "\/" ((b ` ) "/\" (c ` )) & ((a ` ) "/\" ((b ` ) "/\" (c ` ))) "\/" ((a ` ) "/\" (b "/\" c)) = (a ` ) "/\" (((b ` ) "/\" (c ` )) "\/" (b "/\" c)) & (Top B) "/\" (((b ` ) "/\" (c ` )) "\/" (b "/\" c)) = ((b ` ) "/\" (c ` )) "\/" (b "/\" c) & ((a "/\" (((b ` ) "/\" (c ` )) "\/" (b "/\" c))) "\/" ((a ` ) "/\" ((b ` ) "/\" (c ` )))) "\/" ((a ` ) "/\" (b "/\" c)) = (a "/\" (((b ` ) "/\" (c ` )) "\/" (b "/\" c))) "\/" (((a ` ) "/\" ((b ` ) "/\" (c ` ))) "\/" ((a ` ) "/\" (b "/\" c))) & a "\/" (a ` ) = Top B & (a "/\" (((b ` ) "/\" (c ` )) "\/" (b "/\" c))) "\/" ((a ` ) "/\" (((b ` ) "/\" (c ` )) "\/" (b "/\" c))) = (a "\/" (a ` )) "/\" (((b ` ) "/\" (c ` )) "\/" (b "/\" c)) ) by LATTICES:18, LATTICES:43, LATTICES:48, LATTICES:def 5, LATTICES:def 7, LATTICES:def 11;
then A2: ( (a <=> b) <=> (a <=> c) = b <=> c & B is I_Lattice ) by A1, Th51, FILTER_0:40;
assume a <=> b = a <=> c ; :: thesis: b = c
then ( (a <=> b) => (a <=> c) = Top B & (a <=> c) => (a <=> b) = Top B ) by A2, FILTER_0:38;
then b <=> c = Top B by A2, LATTICES:18;
then ( Top B [= b => c & Top B [= c => b ) by LATTICES:23;
then ( b "/\" (Top B) [= b "/\" (b => c) & c "/\" (Top B) [= c "/\" (c => b) & b "/\" (b => c) [= c & c "/\" (c => b) [= b & b "/\" (Top B) = b & c "/\" (Top B) = c ) by A2, FILTER_0:def 8, LATTICES:27, LATTICES:43;
then ( b [= c & c [= b ) by LATTICES:25;
hence b = c by LATTICES:26; :: thesis: verum