let p, q be Element of HP-WFF ; :: thesis: ( p '&' q <> p & p '&' q <> q )
( len p < len (p '&' q) & len q < len (p '&' q) ) by Th15;
hence ( p '&' q <> p & p '&' q <> q ) ; :: thesis: verum