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