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 b9c9 = (b `) "/\" (c `);
set a9b9 = (a `) "/\" (b `);
set a9c9 = (a `) "/\" (c `);
set a9b = (a `) "/\" b;
set a9c = (a `) "/\" c;
set ab9 = a "/\" (b `);
set ac9 = a "/\" (c `);
A1: (a <=> b) <=> (a <=> c) = ((a <=> b) "/\" (a <=> c)) "\/" (((a <=> b) `) "/\" ((a <=> c) `)) by Th50;
B1: ( a <=> b = (a "/\" b) "\/" ((a `) "/\" (b `)) & a <=> c = (a "/\" c) "\/" ((a `) "/\" (c `)) ) by Th50;
C1: (a <=> b) ` = (a "/\" (b `)) "\/" ((a `) "/\" b) by Th51;
D1: (a <=> c) ` = (a "/\" (c `)) "\/" ((a `) "/\" c) by Th51;
E1: ((a "/\" b) "\/" ((a `) "/\" (b `))) "/\" ((a "/\" c) "\/" ((a `) "/\" (c `))) = ((a "/\" b) "/\" ((a "/\" c) "\/" ((a `) "/\" (c `)))) "\/" (((a `) "/\" (b `)) "/\" ((a "/\" c) "\/" ((a `) "/\" (c `)))) by LATTICES:def 11;
F1: ( (a "/\" b) "/\" ((a "/\" c) "\/" ((a `) "/\" (c `))) = ((a "/\" b) "/\" (a "/\" c)) "\/" ((a "/\" b) "/\" ((a `) "/\" (c `))) & (a "/\" b) "/\" ((a `) "/\" (c `)) = ((a "/\" b) "/\" (a `)) "/\" (c `) ) by LATTICES:def 7, LATTICES:def 11;
G1: ((a `) "/\" (b `)) "/\" ((a "/\" c) "\/" ((a `) "/\" (c `))) = (((a `) "/\" (b `)) "/\" (a "/\" c)) "\/" (((a `) "/\" (b `)) "/\" ((a `) "/\" (c `))) by LATTICES:def 11;
H1: (b "/\" a) "/\" (a `) = b "/\" (a "/\" (a `)) by LATTICES:def 7;
L1: (b `) "/\" (Bottom B) = Bottom B ;
R1: ((a `) "/\" (b `)) "/\" (a "/\" c) = (((a `) "/\" (b `)) "/\" a) "/\" c by LATTICES:def 7;
S1: ((b `) "/\" (a `)) "/\" a = (b `) "/\" ((a `) "/\" a) by LATTICES:def 7;
T1: ((a "/\" b) "/\" (a "/\" c)) "\/" (Bottom B) = (a "/\" b) "/\" (a "/\" c) ;
U1: (Bottom B) "\/" (((a `) "/\" (b `)) "/\" ((a `) "/\" (c `))) = ((a `) "/\" (b `)) "/\" ((a `) "/\" (c `)) ;
V1: ((a "/\" (b `)) "\/" ((a `) "/\" b)) "/\" ((a "/\" (c `)) "\/" ((a `) "/\" c)) = ((a "/\" (b `)) "/\" ((a "/\" (c `)) "\/" ((a `) "/\" c))) "\/" (((a `) "/\" b) "/\" ((a "/\" (c `)) "\/" ((a `) "/\" c))) by LATTICES:def 11;
X1: ( (a "/\" (b `)) "/\" ((a "/\" (c `)) "\/" ((a `) "/\" c)) = ((a "/\" (b `)) "/\" (a "/\" (c `))) "\/" ((a "/\" (b `)) "/\" ((a `) "/\" c)) & (a "/\" (b `)) "/\" ((a `) "/\" c) = ((a "/\" (b `)) "/\" (a `)) "/\" c ) by LATTICES:def 7, LATTICES:def 11;
Y1: ((a `) "/\" b) "/\" ((a "/\" (c `)) "\/" ((a `) "/\" c)) = (((a `) "/\" b) "/\" (a "/\" (c `))) "\/" (((a `) "/\" b) "/\" ((a `) "/\" c)) by LATTICES:def 11;
I1: ((b `) "/\" a) "/\" (a `) = (b `) "/\" (a "/\" (a `)) by LATTICES:def 7;
J1: ( 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 LATTICES:20, LATTICES:def 7;
( (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:21, LATTICES:def 5, LATTICES:def 7, LATTICES:def 11;
then A2: (a <=> b) <=> (a <=> c) = b <=> c by B1, A1, Th50, C1, D1, E1, F1, G1, H1, I1, J1, L1, R1, S1, T1, U1, V1, X1, Y1;
assume A3: a <=> b = a <=> c ; :: thesis: b = c
then B4: (a <=> b) => (a <=> c) = Top B by FILTER_0:28;
((a <=> b) => (a <=> b)) "/\" ((a <=> b) => (a <=> b)) = (a <=> b) => (a <=> b) ;
then A4: b <=> c = Top B by A2, A3, B4;
then A5: b "/\" (Top B) [= b "/\" (b => c) by LATTICES:6, LATTICES:9;
A6: c "/\" (Top B) [= c "/\" (c => b) by A4, LATTICES:6, LATTICES:9;
A7: b "/\" (b => c) [= c by FILTER_0:def 7;
A8: c "/\" (c => b) [= b by FILTER_0:def 7;
A11: b [= c by A5, A7, LATTICES:7;
c [= b by A6, A8, LATTICES:7;
hence b = c by A11, LATTICES:8; :: thesis: verum