let A be set ; :: thesis: for a, b being Element of (NormForm A) holds a "\/" b = b "\/" a
set G = NormForm A;
let a, b be Element of (NormForm A); :: thesis: a "\/" b = b "\/" a
reconsider a' = a, b' = b as Element of Normal_forms_on A by Def14;
a "\/" b = mi (b' \/ a') by Def14
.= b "\/" a by Def14 ;
hence a "\/" b = b "\/" a ; :: thesis: verum