let L be non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' LattStr ; :: thesis: for x, y being Element of L holds
( x is_a_complement'_of y iff x is_a_complement_of y )
let x, y be Element of L; :: thesis: ( x is_a_complement'_of y iff x is_a_complement_of y )

hereby :: thesis: ( x is_a_complement_of y implies x is_a_complement'_of y )

assume x is_a_complement'_of y ; :: thesis: x is_a_complement_of y
then ( x "\/" y = Top' L & y "\/" x = Top' L & x "/\" y = Bot' L & y "/\" x = Bot' L ) by Def6;
then ( x "\/" y = Top L & y "\/" x = Top L & x "/\" y = Bottom L & y "/\" x = Bottom L ) by Th19, Th20;
hence x is_a_complement_of y by LATTICES:def 18; :: thesis: verum

end;

assume x is_a_complement_of y ; :: thesis: x is_a_complement'_of y
then ( x "\/" y = Top L & y "\/" x = Top L & x "/\" y = Bottom L & y "/\" x = Bottom L ) by LATTICES:def 18;
then ( x "\/" y = Top' L & y "\/" x = Top' L & x "/\" y = Bot' L & y "/\" x = Bot' L ) by Th19, Th20;
hence x is_a_complement'_of y by Def6; :: thesis: verum