let l be Lattice; :: thesis: for a, b being Element of l holds
( a is_a_complement_of b iff ( a "\/" b = Top l & a "/\" b = Bottom l ) )
let a, b be Element of l; :: thesis: ( a is_a_complement_of b iff ( a "\/" b = Top l & a "/\" b = Bottom l ) )
( ( not a "\/" b = Top l or not a "/\" b = Bottom l ) implies not a is_a_complement_of b )

proof

assume ( not a "\/" b = Top l or not a "/\" b = Bottom l ) ; :: thesis: not a is_a_complement_of b
hence ( not a "\/" b = Top l or not b "\/" a = Top l or not a "/\" b = Bottom l or not b "/\" a = Bottom l ) ; :: according to LATTICES:def 18 :: thesis: verum

end;

hence ( a is_a_complement_of b implies ( a "\/" b = Top l & a "/\" b = Bottom l ) ) ; :: thesis: ( a "\/" b = Top l & a "/\" b = Bottom l implies a is_a_complement_of b )
assume ( a "\/" b = Top l & a "/\" b = Bottom l ) ; :: thesis: a is_a_complement_of b
hence ( a "\/" b = Top l & b "\/" a = Top l & a "/\" b = Bottom l & b "/\" a = Bottom l ) ; :: according to LATTICES:def 18 :: thesis: verum