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