let p, q be boolean object ; :: thesis: (p 'or' q) <=> (q 'or' p) = TRUE
A1: ( p = TRUE or p = FALSE ) by XBOOLEAN:def 3;
( q = TRUE or q = FALSE ) by XBOOLEAN:def 3;
hence (p 'or' q) <=> (q 'or' p) = TRUE by A1; :: thesis: verum