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 a9 = a, b9 = b as Element of Normal_forms_on A by Def12;

a "\/" b = mi (b9 \/ a9) by Def12

.= b "\/" a by Def12 ;

hence a "\/" b = b "\/" a ; :: thesis: verum

set G = NormForm A;

let a, b be Element of (NormForm A); :: thesis: a "\/" b = b "\/" a

reconsider a9 = a, b9 = b as Element of Normal_forms_on A by Def12;

a "\/" b = mi (b9 \/ a9) by Def12

.= b "\/" a by Def12 ;

hence a "\/" b = b "\/" a ; :: thesis: verum