let A be set ; :: thesis: for a, b, c being Element of (NormForm A) holds a "\/" (b "\/" c) = (a "\/" b) "\/" c
set G = NormForm A;
let a, b, c be Element of (NormForm A); :: thesis: a "\/" (b "\/" c) = (a "\/" b) "\/" c
reconsider a9 = a, b9 = b, c9 = c as Element of Normal_forms_on A by Def12;
a "\/" (b "\/" c) = the L_join of (NormForm A) . (a,(mi (b9 \/ c9))) by Def12
.= mi ((mi (b9 \/ c9)) \/ a9) by Def12
.= mi (a9 \/ (b9 \/ c9)) by Th44
.= mi ((a9 \/ b9) \/ c9) by XBOOLE_1:4
.= mi ((mi (a9 \/ b9)) \/ c9) by Th44
.= the L_join of (NormForm A) . ((mi (a9 \/ b9)),c9) by Def12
.= (a "\/" b) "\/" c by Def12 ;
hence a "\/" (b "\/" c) = (a "\/" b) "\/" c ; :: thesis: verum