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