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 Th18;
hence not <^a,b^> is empty ; :: thesis: verum