let L be D_Lattice; :: thesis: for a, b being Element of L st not b [= a holds
<.b.) in (SF_have b) \ (SF_have a)
let a, b be Element of L; :: thesis: ( not b [= a implies <.b.) in (SF_have b) \ (SF_have a) )
assume not b [= a ; :: thesis: <.b.) in (SF_have b) \ (SF_have a)
then not a in <.b.) by FILTER_0:15;
then A1: not <.b.) in SF_have a by Th16;
b in <.b.) ;
then <.b.) in SF_have b ;
hence <.b.) in (SF_have b) \ (SF_have a) by A1, XBOOLE_0:def 5; :: thesis: verum