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 a' = a, b' = b, c' = c as Element of Normal_forms_on A by Def14;
a "\/" (b "\/" c) = the L_join of (NormForm A) . a,(mi (b' \/ c')) by Def14
.= mi ((mi (b' \/ c')) \/ a') by Def14
.= mi (a' \/ (b' \/ c')) by Th68
.= mi ((a' \/ b') \/ c') by XBOOLE_1:4
.= mi ((mi (a' \/ b')) \/ c') by Th68
.= the L_join of (NormForm A) . (mi (a' \/ b')),c' by Def14
.= (a "\/" b) "\/" c by Def14 ;
hence a "\/" (b "\/" c) = (a "\/" b) "\/" c ; :: thesis: verum