consider f being directed-sups-preserving Function of (latt a),(latt b);
f in <^a,b^> by Th15;
hence not <^a,b^> is empty ; :: thesis: verum